Abstract
Invariant Based Programming (IBP) is a formal method in which the invariants are developed before the code. IBP leads to programs that are correct by construction, provides a light formalism that is easy to learn, and supports teaching formal methods. However, like other verification methods it generates a large number of lemmas to be proved. The Socos tool provides automatic verification of invariant based programs: it sends the proof obligations to an automatic theorem prover and reports only the unproven conditions. The latter may be proved interactively in a proof assistant.
In this paper, we describe the Socos embedding of invariant based programs into the theorem prover PVS. The tool generates verification conditions and applies a strategy to decompose the conditions into fine grained lemmas. Each lemma is then attacked with the SMT solver Yices. Socos supports incremental development and allows reasoning in arbitrary program domains through the use of background theories. A background theory is a PVS theory pertaining to a specific programming domain. We give an example of a verification in our system, which demonstrates how background theories improve the degree of proof automation. This work is a step towards scaling up IBP by allowing existing collections of PVS theories to be used.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Back, R.-J.: Invariant based programming: Basic approach and teaching experience. Formal Aspects of Computing 21(3), 227–244 (2009)
Back, R.-J., Eriksson, J., Myreen, M.: Testing and verifying invariant based programs in the SOCOS environment. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 61–78. Springer, Heidelberg (2007)
Back, R.-J., Myreen, M.: Tool support for invariant based programming. In: Proc. of APSEC 2005, pp. 711–718. IEEE Computer Society, Los Alamitos (2005)
Back, R.-J., Preoteasa, V.: Semantics and proof rules of invariant based programs. Technical Report 903, TUCS, Turku, Finland (July 2008)
Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Cormen, T.H., Stein, C., Rivest, R.L., Leiserson, C.E.: Introduction to Algorithms. McGraw-Hill Higher Education, New York (2001)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. of the ACM 52(3), 365–473 (2005)
Dutertre, B., de Moura, L.: The Yices SMT solver. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA (August 2006)
Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007), http://dx.doi.org/10.1007/978-3-540-73368-3_21
Munõz, C.: Batch proving and proof scripting in PVS. Technical Report NASA CR-2007-214546 / NIA 2007-03, NASA Langley Research Center and National Institute of Aerospace (2007)
Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference, (Version 2.4). Computer Science Laboratory, SRI International, Menlo Park, CA (November 2001)
Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: 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)
van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eriksson, J., Back, RJ. (2010). Applying PVS Background Theories and Proof Strategies in Invariant Based Programming. In: Dong, J.S., Zhu, H. (eds) Formal Methods and Software Engineering. ICFEM 2010. Lecture Notes in Computer Science, vol 6447. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16901-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-16901-4_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16900-7
Online ISBN: 978-3-642-16901-4
eBook Packages: Computer ScienceComputer Science (R0)