A Proof Framework for Concurrent Programs

  • Leonard Lensink
  • Sjaak Smetsers
  • Marko van Eekelen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7321)


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.


Model Checker Theorem Prove Global Variable Critical Section Concurrent Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Archer, M.: TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics and Artificial Intelligence (2000)Google Scholar
  2. 2.
    Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press (2008)Google Scholar
  3. 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)CrossRefGoogle Scholar
  4. 4.
    de Groot, A.: Practical Automaton Proofs in PVS. PhD thesis, Radboud University Nijmegen (2008)Google Scholar
  5. 5.
    Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)MathSciNetCrossRefGoogle Scholar
  6. 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)CrossRefGoogle Scholar
  7. 7.
    Lamport, L.: A New Solution of Dijkstra’s Concurrent Programming Problem. Commun. ACM 17(8), 453–455 (1974)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Software Tools for Technology Transfer 1(1-2), 134–152 (1997)zbMATHCrossRefGoogle Scholar
  9. 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)CrossRefGoogle Scholar
  10. 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)Google Scholar
  11. 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)Google Scholar
  12. 12.
    Ripon, S., Miller, A.: Verification of symmetry detection using pvs. ECEASST 35 (2010)Google Scholar
  13. 13.
    Sutter, H.: The Free Lunch Is Over: A Fundamental Turn Toward Concurrency in Software. Dr. Dobb’s Journal 30(3) (March 2005)Google Scholar
  14. 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)CrossRefGoogle Scholar
  15. 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)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Leonard Lensink
    • 1
  • Sjaak Smetsers
    • 1
  • Marko van Eekelen
    • 1
  1. 1.ICISRadboud University NijmegenThe Netherlands

Personalised recommendations