Abstract
A program verifier is a complex system that uses compiler technology, program semantics, property inference, verification-condition generation, automatic decision procedures, and a user interface. This paper describes the architecture of a state-of-the-art program verifier for object-oriented programs.
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
Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling 4(1), 32–54 (2005)
Jean-Raymond, A.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Ambler, A.L., Good, D.I., Browne, J.C., Burger, W.F., Cohen, R.M., Hoch, C.G., Wells, R.E.: GYPSY: A language for specification and implementation of verifiable programs. SIGPLAN Notices 12(3), 1–10 (1977)
Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)
van den Berg, J., Berg, B.J.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)
Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Workshop on Program Analysis for Software Tools and Engineering (PASTE), pp. 82–87 (2005)
Ball, T., Lahiri, S., Musuvathi, M.: Zap: Automated theorem proving for software analysis. Technical Report MSR-TR-2005-137, Microsoft Research (October 2005)
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–60. Springer, Heidelberg (2005)
Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 54–84. Springer, Heidelberg (2004)
Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: a developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)
Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence 7, 23–50 (1972)
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Fourth ACM Symposium on Principles of Programming Languages (POPL), pp. 238–252 (January 1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Sixth ACM Symposium on Principles of Programming Languages (POPL), pp. 269–282 (January 1979)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems 13(4), 451–490 (1991)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Fifth ACM Symposium on Principles of Programming Languages (POPL), pp. 84–96 (January 1978)
Bor-Yuh, E.C., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 147–163. Springer, Heidelberg (2005)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (March 2005)
Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (December 1998)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of the ACM 52(3), 365–473 (2005)
Escher Technologies. Perfect Developer (2006), http://eschertech.com/
Filliâtre, J.-C.: Verification of non-functional programs using interpretations in type theory. The Journal of Functional Programming 13(4), 709–745 (2003)
Fitzgerald, R., Knoblock, T.B., Ruf, E., Steensgaard, B., Tarditi, D.: Marmot: An Optimizing Compiler For Java. Software—Practice and Experience 30(3), 199–232 (2000)
Fähndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: Crocker, R., Steele Jr., G.L. (eds.) Object-Oriented Programming Systems, Languages and Applications (OOPSLA), pp. 302–312. ACM, New York (2003)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Programming Language Design and Implementation (PLDI), pp. 234–245 (2002)
Filliâtre, J.-C., Marché, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004)
Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 193–205. ACM, New York (2001)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580,583 (1969)
Hoare, C.A.R., Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informatica 2(4), 335–355 (1973)
Jacobs, B.: Weakest pre-condition reasoning for Java programs with JML annotations. Journal of Logic and Algebraic Programming 58(1–2), 61–88 (2004)
Jacobs, B., Poll, E.: A logic for the Java Modeling Language JML. In: Hussmann, H. (ed.) ETAPS 2001 and FASE 2001. LNCS, vol. 2029, pp. 284–299. Springer, Heidelberg (2001)
Jacobs, B., Poll, E.: Java program verification at Nijmegen: Developments and perspective. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 134–153. Springer, Heidelberg (2004)
Cok, D.R., Kiniry, J.R.: ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)
Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer Academic Publishers, Boston (1999)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06u, Iowa State University, Department of Computer Science (April 2003)
Leino, K.R.M.: Toward Reliable Modular Programs. PhD thesis, CalTech, Available as Technical Report Caltech-CS-TR-95-03 (1995)
Leino, K.R.M.: Extended static checking: A ten-year perspective. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, p. 157. Springer, Heidelberg (2001)
Leino, K.R.M.: Efficient weakest preconditions. Information Processing Letters 93(6), 281–288 (2005)
Lampson, B.W., Horning, J.J., London, R.L., Mitchell, J.G., Popek, G.J.: Report on the programming language Euclid. Technical Report CSL-81-12, Xerox PARC (October 1981); An earlier version of this report appeared. SIGPLAN Notices, vol. 12(2). ACM, New York (February 1977)
Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 119–134. Springer, Heidelberg (2005)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–516. Springer, Heidelberg (2004)
Leino, K.R.M., Müller, P.: Modular verification of static class invariants. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 26–42. Springer, Heidelberg (2005)
Leino, K.R.M., Müller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 115–130. Springer, Heidelberg (2006)
Leino, K.R.M., Millstein, T., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Science of Computer Programming 55(1–3), 209–226 (2005)
Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems 24(5), 491–553 (2002)
Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In: Aichernig, B.K., Beckert, B. (eds.) Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), pp. 2–12. IEEE Computer Society, Los Alamitos (2005)
Rustan, K., Leino, M., Saxe, J.B., Stata, R.: Checking Java programs via guarded commands. Formal Techniques for Java Programs, Technical Report 251. Fernuniversität Hagen (May 1999); Also available as Technical Note 1999-002, Compaq Systems Research Center
Meyer, B.: Eiffel: The Language. Object-Oriented Series. Prentice-Hall, Englewood Cliffs (1992)
Miné, A.: The octagon abstract domain. In: Working Conference on Reverse Engineering (WCRE), pp. 310–319 (2001)
Müller, P., Meyer, J., Poetzsch-Heffter, A.: Programming and interface specification language of Jive—specification and design rationale. Technical Report 223, Fernuniversität Hagen(1997)
Marché, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming 58(1–2), 89–106 (2004)
Nelson, G.: A generalization of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems 11(4), 517–561 (1989)
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)
Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitationsschrift, Technische Universität München (1997)
Reynolds, J.C.: Syntactic control of interference. In: Fifth ACM Symposium on Principles of Programming Languages (POPL), pp. 39–46 (January 1978)
Rosenblum, D.S.: A practical approach to programming with assertions. IEEE Transactions on Software Engineering 21(1), 19–31 (1995)
Spec# homepage (2006), http://research.microsoft.com/specsharp
Vandevoorde, M.T.: Exploiting Specifications to Improve Program Performance. In: PhD thesis, Massachusetts Institute of Technology (February 1994); Available as Technical Report MIT/LCS/TR-598
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barnett, M., Chang, BY.E., DeLine, R., Jacobs, B., Leino, K.R.M. (2006). Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2005. Lecture Notes in Computer Science, vol 4111. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11804192_17
Download citation
DOI: https://doi.org/10.1007/11804192_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-36749-9
Online ISBN: 978-3-540-36750-5
eBook Packages: Computer ScienceComputer Science (R0)