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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Archer, M.: TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics and Artificial Intelligence (2000)
Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press (2008)
Basten, T., Hooman, J.: Process Algebra in PVS. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 270–284. Springer, Heidelberg (1999)
de Groot, A.: Practical Automaton Proofs in PVS. PhD thesis, Radboud University Nijmegen (2008)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
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)
Lamport, L.: A New Solution of Dijkstra’s Concurrent Programming Problem. Commun. ACM 17(8), 453–455 (1974)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Software Tools for Technology Transfer 1(1-2), 134–152 (1997)
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)
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)
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)
Ripon, S., Miller, A.: Verification of symmetry detection using pvs. ECEASST 35 (2010)
Sutter, H.: The Free Lunch Is Over: A Fundamental Turn Toward Concurrency in Software. Dr. Dobb’s Journal 30(3) (March 2005)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lensink, L., Smetsers, S., van Eekelen, M. (2012). A Proof Framework for Concurrent Programs. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds) Integrated Formal Methods. IFM 2012. Lecture Notes in Computer Science, vol 7321. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30729-4_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-30729-4_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30728-7
Online ISBN: 978-3-642-30729-4
eBook Packages: Computer ScienceComputer Science (R0)