Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1007/978-3-642-30729-4_13guideproceedingsArticle/Chapter ViewAbstractPublication PagesConference Proceedingsacm-pubtype
Article

A proof framework for concurrent programs

Published: 15 June 2012 Publication History

Abstract

This paper presents a proof framework for verifying concurrent programs that communicate using global variables. The approach is geared towards verification of models that have an unbounded state size and are as close to the original code as possible. The bakery algorithm is used as a demonstration of the framework basics, while the (full) framework with thread synchronization was used to verify and correct the reentrant readers writers algorithm as used in the Qt library.

References

[1]
Archer, M.: TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics and Artificial Intelligence (2000)
[2]
Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press (2008)
[3]
Basten, T., Hooman, J.: Process Algebra in PVS. In: Cleaveland, W. R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 270-284. Springer, Heidelberg (1999)
[4]
de Groot, A.: Practical Automaton Proofs in PVS. PhD thesis, Radboud University Nijmegen (2008)
[5]
Holzmann, G. J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279-295 (1997)
[6]
Katz, S.: Faithful Translations among Models and Specifications. In: Oliveira, J., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 419-434. Springer, Heidelberg (2001)
[7]
Lamport, L.: A New Solution of Dijkstra's Concurrent Programming Problem. Commun. ACM 17(8), 453-455 (1974)
[8]
Larsen, K. G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Software Tools for Technology Transfer 1(1-2), 134-152 (1997)
[9]
Owre, S., Rajan, S., Rushby, J., Shankar, N., Srivas, M.: PVS: Combining Specification, Proof Checking, and Model Checking. In: Alur, R., Henzinger, T. A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411-414. Springer, Heidelberg (1996)
[10]
Owre, S., Rushby, J. M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 747-752. Springer, Heidelberg (1992)
[11]
Pantelic, V., Jin, X.-H., Lawford, M., Parnas, D. L.: Inspection of concurrent systems: Combining tables, theorem proving and model checking. In: Software Engineering Research and Practice, pp. 629-635 (2006)
[12]
Ripon, S., Miller, A.: Verification of symmetry detection using pvs. ECEASST 35 (2010)
[13]
Sutter, H.: The Free Lunch Is Over: A Fundamental Turn Toward Concurrency in Software. Dr. Dobb's Journal 30(3) (March 2005)
[14]
van Gastel, B., Lensink, L., Smetsers, S., van Eekelen, M.: Reentrant Readers-Writers: A Case Study Combining Model Checking with Theorem Proving. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 85-102. Springer, Heidelberg (2009)
[15]
van Gastel, B., Lensink, L., Smetsers, S., van Eekelen, M.: Deadlock and Starvation Free Reentrant Readers-Writers. Sci. Comput. Program. 76(2), 82-99 (2011)

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings
IFM'12: Proceedings of the 9th international conference on Integrated Formal Methods
June 2012
357 pages
ISBN:9783642307287
  • Editors:
  • John Derrick,
  • Stefania Gnesi,
  • Diego Latella,
  • Helen Treharne

Sponsors

  • INTECS: INTECS S.p.A.
  • FME: Formal Methods Europe
  • EATCS: European Association for Theoretical Computer Science
  • BNL: Banca Nazionale del Lavoro S.p.A.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 15 June 2012

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • 0
    Total Citations
  • 0
    Total Downloads
  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 16 Dec 2024

Other Metrics

Citations

View Options

View options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media