×

Verification conditions for source-level imperative programs. (English) Zbl 1298.68171

Summary: This paper is a systematic study of verification conditions and their use in the context of program verification. We take Hoare logic as a starting point and study in detail how a verification conditions generator can be obtained from it. The notion of program annotation is essential in this process. Weakest preconditions and the use of updates are also studied as alternative approaches to verification conditions. Our study is carried on in the context of a While language. Important extensions to this language are considered toward the end of the paper. We also briefly survey modern program verification tools and their approaches to the generation of verification conditions.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68-02 Research exposition (monographs, survey articles) pertaining to computer science
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Igarashi, Shigeru; London, Ralph L.; Luckham, David C., Automatic program verification I: a logical basis and its implementation, Acta Inf., 4, 145-182 (1974) · Zbl 0279.68022
[2] Donald I. Good, Mechanical proofs about computer programs. Technical Report 41, The University of Texas at Austin, March 1984.; Donald I. Good, Mechanical proofs about computer programs. Technical Report 41, The University of Texas at Austin, March 1984. · Zbl 0544.68012
[3] James Cornelius King, A Program Verifier. Ph.D. Thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 1969.; James Cornelius King, A Program Verifier. Ph.D. Thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 1969.
[4] Boyer, R. S.; Moore, J. S., The Correctness Problem in Computer Science, Chapter A Verification Condition Generator for FORTRAN (1981), Academic Press
[5] Dwyer, Matthew B.; Hatcliff, John; Robby, Robby; Pasareanu, Corina S.; Visser, Willem, Formal software analysis emerging trends in software model checking, (2007 Future of Software Engineering, FOSE ’07 (2007), IEEE Computer Society: IEEE Computer Society Washington, DC, USA), 120-136
[6] D’Silva, Vijay; Kroening, Daniel; Weissenbacher, Georg, A survey of automated techniques for formal software verification, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 27, 7, 1165-1178 (2008)
[7] Jhala, Ranjit; Majumdar, Rupak, Software model checking, ACM Comput. Surv., 41, October, 21:1-21:54 (2009) · Zbl 1507.68188
[8] Patrick Cousot, Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, January 1977, pp. 238-252.; Patrick Cousot, Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, January 1977, pp. 238-252. · Zbl 1149.68389
[9] Necula, G. C., Proof-carrying code, (Proceedings of POPL’97 (1997), ACM Press), 106-119
[10] Sabelfeld, A.; Myers, A., Language-based information-flow security, IEEE Journal on Selected Areas in Communications, 21, 1 (2003)
[11] Barthe, Gilles; D’Argenio, Pedro R.; Rezk, Tamara, Secure information flow by self-composition, (CSFW (2004), IEEE Computer Society), 100-114 · Zbl 1252.68072
[12] Darvas, Ádám; Hähnle, Reiner; Sands, David, A theorem proving approach to analysis of secure information flow, (Hutter, Dieter; Ullmann, Markus, SPC. SPC, Lecture Notes in Computer Science, vol. 3450 (2005), Springer), 193-209
[13] Loeckx, Jacques; Sieber, Kurt, The Foundations of Program Verification (1987), John Wiley & Sons, Inc.: John Wiley & Sons, Inc. New York, NY, USA · Zbl 0625.68017
[14] Winskel, Glynn, The formal semantics of programming languages: an introduction, (Foundations of Computing (1993), The MIT Press: The MIT Press Cambridge, Massachusetts) · Zbl 0919.68082
[15] Reynolds, John C., Theories of Programming Languages (1998), Cambridge University Press: Cambridge University Press Cambridge, England · Zbl 0972.68507
[16] Gries, David, The Science of Programming (1987), Springer-Verlag New York, Inc.: Springer-Verlag New York, Inc. Secaucus, NJ, USA · Zbl 0614.68002
[17] Hoare, C. A.R., An axiomatic basis for computer programming, Communications of the ACM, 12, 576-580 (1969) · Zbl 0179.23105
[18] Floyd, Robert, Assigning meaning to programs, (Schwartz, J. T., Mathematical Aspects of Computer Science, Number 19 in Proceedings of Symposia in Applied Mathematics (1967), American Mathematical Society), 19-32
[19] Apt, Krzysztof R., Ten years of Hoare’s logic: a survey — part 1, ACM Trans. Program. Lang. Syst., 3, 4, 431-483 (1981) · Zbl 0471.68006
[20] Cousot, Patrick, Methods and logics for proving programs, (Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) (1990), Elsevier and MIT Press), 841-994 · Zbl 0900.68307
[21] Jones, Cliff B., The early search for tractable ways of reasoning about programs, IEEE Ann. Hist. Comput., 25, 2, 26-49 (2003)
[22] Backhouse, Roland, Program Construction — Calculating Implementations from Specifications (2003), John Wiley & Sons, Ltd.
[23] Tennent, R. D., Specifying Software (2001), Cambridge University Press: Cambridge University Press New York, NY, USA · Zbl 1006.68035
[24] Yves Bertot, Theorem proving support in programming language semantics. CoRR, abs/0707.0926, 2007.; Yves Bertot, Theorem proving support in programming language semantics. CoRR, abs/0707.0926, 2007. · Zbl 1195.68090
[25] Gordon, Michael J. C., Mechanizing programming logics in higher order logic, (Birtwistle, G.; Subrahmanyam, P. A., Current Trends in Hardware Verification and Automated Theorem Proving (1989), Springer-Verlag New York, Inc.), 387-439
[26] Homeier, Peter V.; Martin, David F., A mechanically verified verification condition generator, Comput. J., 38, 2, 131-141 (1995)
[27] A. Azurat, I.S.W.B. Prasetya, A survey on embedding programming logics in a theorem prover. Technical report, University of Utrecht, 2002.; A. Azurat, I.S.W.B. Prasetya, A survey on embedding programming logics in a theorem prover. Technical report, University of Utrecht, 2002.
[28] Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall: Prentice-Hall Englewood Cliffs, New Jersey · Zbl 0368.68005
[29] Rustan, K.; Leino, M.; Saxe, James B.; Stata, Raymie; Demeyer, Serge, Checking Java programs via guarded commands, (Moreira, Ana M. D., Proceedings of ECOOP Workshops’99. Proceedings of ECOOP Workshops’99, Lecture Notes in Computer Science, vol. 1743 (1999), Springer), 110-111
[30] Rustan, K.; Leino, M., Extended static checking: a ten-year perspective, (Informatics — 10 Years Back. 10 Years Ahead (2001), Springer-Verlag: Springer-Verlag London, UK), 157-175 · Zbl 0997.68562
[31] Cok, David R.; Kiniry, Joseph, ESC/Java2: uniting ESC/Java and JML, (Barthe, Gilles; Burdy, Lilian; Huisman, Marieke; Lanet, Jean-Louis; Muntean, Traian, CASSIS. CASSIS, Lecture Notes in Computer Science, vol. 3362 (2004), Springer), 108-128
[32] Barnett, Michael; Chang, Bor-Yuh Evan; DeLine, Robert; Jacobs, Bart; Leino, K. Rustan M., Boogie: a modular reusable verifier for object-oriented programs, (de Boer, Frank S.; Bonsangue, Marcello M.; Graf, Susanne; de Roever, Willem P., FMCO. FMCO, Lecture Notes in Computer Science, vol. 4111 (2005), Springer), 364-387
[33] Detlefs, David; Nelson, Greg; Saxe, James B., Simplify: a theorem prover for program checking, J. ACM, 52, 3, 365-473 (2005) · Zbl 1323.68462
[34] Barnett, Michael; Rustan, K.; Leino, M., Weakest-precondition of unstructured programs, SIGSOFT Softw. Eng. Notes, 31, 1, 82-87 (2006)
[35] Flanagan, Cormac; Saxe, James B., Avoiding exponential explosion: generating compact verification conditions, (POPL’01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (2001), ACM: ACM New York, NY, USA), 193-205 · Zbl 1323.68372
[36] Rustan, K.; Leino, M., Efficient weakest preconditions, Inf. Process. Lett., 93, 6, 281-288 (2005) · Zbl 1173.68563
[37] Kaldewaij, Anne, Programming: The Derivation of Algorithms (1990), Prentice-Hall, Inc.: Prentice-Hall, Inc. Upper Saddle River, NJ, USA · Zbl 0709.68020
[38] Reiner Hähnle, Richard Bubel, A Hoare-style calculus with explicit state updates. Department of Computer Science, Chalmers University of Technology.; Reiner Hähnle, Richard Bubel, A Hoare-style calculus with explicit state updates. Department of Computer Science, Chalmers University of Technology. · Zbl 1254.68073
[39] Ahrendt, Wolfgang; Baar, Thomas; Beckert, Bernhard; Bubel, Richard; Giese, Martin; Hähnle, Reiner; Menzel, Wolfram; Mostowski, Wojciech; Roth, Andreas; Schlager, Steffen; Schmitt, Peter H., The KeY tool, Software and System Modeling, 4, 1, 32-54 (2005)
[40] Beckert, Bernhard, A dynamic logic for the formal verification of Java Card programs, (Attali, Isabelle; Jensen, Thomas P., Java Card Workshop. Java Card Workshop, Lecture Notes in Computer Science, vol. 2041 (2000), Springer), 6-24 · Zbl 0980.68525
[41] Harel, D.; logic, Dynamic, (Gabbay, D.; Guenther, F., Handbook of Philosophical Logic Volume II — Extensions of Classical Logic (1984), D. Reidel Publishing Company: D. Reidel Publishing Company Dordrecht, The Netherlands), 497-604
[42] O’Hearn, Peter W.; Reynolds, John C.; Yang, Hongseok, Local reasoning about programs that alter data structures, (Proceedings of the 15th International Workshop on Computer Science Logic. Proceedings of the 15th International Workshop on Computer Science Logic, CSL’01 (2001), Springer-Verlag: Springer-Verlag London, UK), 1-19 · Zbl 0999.68045
[43] Reynolds, John C., Separation logic: a logic for shared mutable data structures, (LICS (2002), IEEE Computer Society), 55-74
[44] Burstall, Rod, Some techniques for proving correctness of programs which alter data structures, Machine Intelligence, 7 (1972) · Zbl 0259.68009
[45] Bornat, Richard, Proving pointer programs in Hoare logic, (Backhouse, Roland Carl; Oliveira, José Nuno, MPC. MPC, Lecture Notes in Computer Science, vol. 1837 (2000), Springer), 102-126 · Zbl 0963.68036
[46] Hoare, C. A.R., Procedures and parameters: an axiomatic approach, (Proceeedings of Symposium on Semantics of Algorithmic Languages. Proceeedings of Symposium on Semantics of Algorithmic Languages, Lecture Notes in Mathematics, vol. 188 (1971), Springer: Springer Berlin, Heidelberg) · Zbl 0221.68020
[47] Meyer, Bertrand, Applying “design by contract”, IEEE Computer, 25, 10 (1992)
[48] Homeier, Peter V.; Martin, David F., Mechanical verification of mutually recursive procedures, (McRobbie, Michael A.; Slaney, John K., CADE. CADE, Lecture Notes in Computer Science, vol. 1104 (1996), Springer), 201-215 · Zbl 1075.68615
[49] Kleymann, Thomas, Hoare logic and auxiliary variables, Formal Aspects of Computing, 11, 5, 541-566 (1999) · Zbl 0978.03026
[50] von Oheimb, David, Hoare logic for mutual recursion and local variables, (Foundations of Software Technology and Theoretical Computer Science (1999)), 168-180 · Zbl 0956.68086
[51] Borgida, Alexander; Mylopoulos, John; Reiter, Raymond, On the frame problem in procedure specifications, Software Engineering, 21, 10, 785-798 (1995)
[52] de Moura, Leonardo; Bjrner, Nikolaj, Satisfiability modulo theories: an appetizer, (Medeiros Oliveira, Marcel Vinicius; Woodcock, Jim, SBMF. SBMF, Lecture Notes in Computer Science, vol. 5902 (2009), Springer), 23-36 · Zbl 1266.03047
[53] de Moura, Leonardo; Dutertre, Bruno; Shankar, Natarajan, A tutorial on satisfiability modulo theories, (Proceedings of the 19th International Conference on Computer Aided Verification, CAV’07 (2007), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 20-36 · Zbl 1135.68563
[54] Malik, Sharad; Zhao, Ying; Madigan, Conor F.; Zhang, Lintao; Moskewicz, Matthew W., Chaff: engineering an efficient SAT solver, Design Automation Conference, 0, 530-535 (2001)
[55] En, Niklas; Srensson, Niklas, An extensible SAT-solver, (Giunchiglia, Enrico; Tacchella, Armando, SAT. SAT, Lecture Notes in Computer Science, vol. 2919 (2003), Springer), 502-518 · Zbl 1204.68191
[56] Bruno Dutertre, Leonardo De Moura, The Yices SMT Solver. Technical report, SRI, 2006.; Bruno Dutertre, Leonardo De Moura, The Yices SMT Solver. Technical report, SRI, 2006.
[57] Barrett, Clark; Tinelli, Cesare, CVC3, (Damm, Werner; Hermanns, Holger, Proceedings of the 19th International Conference on Computer Aided Verification. Proceedings of the 19th International Conference on Computer Aided Verification, CAV’07. Proceedings of the 19th International Conference on Computer Aided Verification. Proceedings of the 19th International Conference on Computer Aided Verification, CAV’07, Lecture Notes in Computer Science, vol. 4590 (2007), Springer-Verlag: Springer-Verlag Berlin, Germany), 298-302
[58] de Moura, Leonardo; Bjørner, Nikolaj, (Z3: An Efficient SMT Solver. Z3: An Efficient SMT Solver, Lecture Notes in Computer Science, vol. 4963/2008 (2008), Springer: Springer Berlin), 337-340
[59] Sylvain Conchon, Evelyne Contejean, Johannes Kanig, Ergo: a theorem prover for polymorphic first-order logic modulo theories, 2006.; Sylvain Conchon, Evelyne Contejean, Johannes Kanig, Ergo: a theorem prover for polymorphic first-order logic modulo theories, 2006. · Zbl 1277.68240
[60] Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus, (Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283 (2002), Springer) · Zbl 0994.68131
[61] Bertot, Yves; Castéran, Pierre, (Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science (2004), Springer Verlag) · Zbl 1069.68095
[62] Shankar, Natarajan, Automated deduction for verification, ACM Comput. Surv., 41, October, 20:1-20:56 (2009) · Zbl 1507.68197
[63] German, Steven M.; Wegbreit, Ben, A synthesizer of inductive assertions, (Proceedings of the May 19-22, 1975, National Computer Conference and Exposition. Proceedings of the May 19-22, 1975, National Computer Conference and Exposition, AFIPS’75 (1975), ACM: ACM New York, NY, USA), 369-376
[64] Katz, Shmuel; Manna, Zohar, Logical analysis of programs, Commun. ACM, 19, April, 188-206 (1976) · Zbl 0353.68016
[65] Karr, M., Affine relationships among variables of a program, Acta Informatica, 6, 133-151 (1976) · Zbl 0358.68025
[66] Suzuki, Norihisa; Ishihata, Kiyoshi, Implementation of an array bound checker, (Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL’77 (1977), ACM: ACM New York, NY, USA), 132-143
[67] Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among variables of a program, (Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1978), ACM Press: ACM Press Tucson, Arizona, New York, NY), 84-97
[68] Dershowitz, Nachum; Manna, Zohar, Inference rules for program annotation, (Proceedings of the 3rd international conference on Software engineering. Proceedings of the 3rd international conference on Software engineering, ICSE’78 (1978), IEEE Press: IEEE Press Piscataway, NJ, USA), 158-167 · Zbl 0463.68023
[69] Ernst, Michael D.; Cockrell, Jake; Griswold, William G.; Notkin, David, Dynamically discovering likely program invariants to support program evolution, IEEE Transactions on Software Engineering, 27, 99-123 (2001)
[70] Leavens, Gary T.; Ruby, Clyde; Rustan, K.; Leino, M.; Poll, Erik; Jacobs, Bart, JML: notations and tools supporting detailed design in Java, (OOPSLA’00: Addendum to the 2000 Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications (Addendum) (2000), ACM: ACM New York, NY, USA), 105-106
[71] G. Leavens, Y. Cheon, Design by Contract with JML, 2003.; G. Leavens, Y. Cheon, Design by Contract with JML, 2003.
[72] Poetzsch-Heffter, Arnd; Müller, Peter, A programming logic for sequential Java, (Doaitse Swierstra, S., ESOP. ESOP, Lecture Notes in Computer Science, vol. 1576 (1999), Springer), 162-176
[73] Jacobs, Bart; Kiniry, Joseph; Warnier, Martijn, Java program verification challenges, (de Boer, Frank S.; Bonsangue, Marcello M.; Graf, Susanne; de Roever, Willem P., FMCO. FMCO, Lecture Notes in Computer Science, vol. 2852 (2002), Springer), 202-219
[74] Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter, Specification and verification challenges for sequential object-oriented programs, Form. Asp. Comput., 19, 2, 159-189 (2007) · Zbl 1121.68074
[75] Meyer, J.; Müller, P.; Poetzsch-Heffter, A., The JIVE System—Implementation Description (2000), FernUniversität Hagen
[76] Owre, Sam; Rushby, John M.; Shankar, Natarajan, PVS: a prototype verification system, (Kapur, Deepak, CADE. CADE, Lecture Notes in Computer Science, vol. 607 (1992), Springer), 748-752
[77] Jacobs, Bart; Poll, Erik, A logic for the Java modeling language JML, (Hußmann, Heinrich, FASE. FASE, Lecture Notes in Computer Science, vol. 2029 (2001), Springer), 284-299 · Zbl 0977.68588
[78] Jacobs, Bart, Weakest pre-condition reasoning for Java programs with JML annotations, J. Log. Algebr. Program., 58, 1-2, 61-88 (2004) · Zbl 1073.68024
[79] von Oheimb, David, Hoare logic for Java in Isabelle/HOL, Concurrency and Computation: Practice and Experience, 13, 13, 1173-1214 (2001) · Zbl 0997.68019
[80] Filliâtre, Jean-Christophe; Marché, Claude, The Why/Krakatoa/Caduceus platform for deductive program verification, (Damm, Werner; Hermanns, Holger, Proceedings of CAV’07. Proceedings of CAV’07, Lecture Notes in Computer Science, vol. 4590 (2007), Springer), 173-177
[81] Filliâtre, Jean-Christophe; Marché, Claude, Multi-prover verification of C programs, (Davies, Jim; Schulte, Wolfram; Barnett, Michael, ICFEM. ICFEM, Lecture Notes in Computer Science, vol. 3308 (2004), Springer), 15-29
[82] Loc Correnson, Pascal Cuoq, Armand Puccetti, Julien Signoles, Frama-C user manual. Available from the Frama-C website, 2010, http://frama-c.com; Loc Correnson, Pascal Cuoq, Armand Puccetti, Julien Signoles, Frama-C user manual. Available from the Frama-C website, 2010, http://frama-c.com
[83] Marché, Claude; Paulin-Mohring, Christine; Urbain, Xavier, The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML, J. Log. Algebr. Program., 58, 1-2, 89-106 (2004) · Zbl 1073.68678
[84] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, Virgile Prevosto, ACSL: ANSI/ISO C Specification Language. CEA LIST and INRIA, 2010.; Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, Virgile Prevosto, ACSL: ANSI/ISO C Specification Language. CEA LIST and INRIA, 2010.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.