Abstract
Intermediate languages are a paradigm to separate concerns in software verification systems when bridging the gap between programming languages and the logics understood by theorem provers. While such intermediate languages traditionally only offer rather simple type systems, this paper argues that it is both advantageous and feasible to integrate richer type systems with features like (higher-ranked) polymorphism and quantification over types. As a concrete solution, the paper presents the type system of Boogie 2, an intermediate verification language that is used in several program verifiers. The paper gives two encodings of types and formulae in simply typed logic such that SMT solvers and other theorem provers can be used to discharge verification conditions.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2008), www.SMT-LIB.org
Bobot, F., Conchon, S., Contejean, E., Lescuyer, S.: Implementing polymorphism in SMT solvers. In: SMT 2008 (2008)
Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamarić, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007)
Cohen, E., Moskal, M., Schulte, W., Tobies, S.: A practical verification methodology for concurrent programs. MSR-TR 2009-15, Microsoft Research (2009)
Couchot, J.F., Lescuyer, S.: Handling polymorphism in automated deduction. In: CADE-21, pp. 263–278 (2007)
Dahn, I.: Interpretation of a Mizar-like logic in first-order logic. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 137–151. Springer, Heidelberg (2000)
DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. MSR-TR 2005-70, Microsoft Research (March 2005)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
Filliâtre, J.C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud (March 2003)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI 2002. ACM, New York (2002)
Hurd, J.: First-order proof tactics in higher-order logic theorem provers. Technical Report NASA/CP-2003-212448, pp. 56–68 (2003)
Leino, K.R.M.: This is Boogie 2. Manuscript KRML 178 (2008), http://research.microsoft.com/~leino/papers.html
Leino, K.R.M.: Specification and verification of object-oriented software. In: Summer School Marktoberdorf 2008. NATO ASI Series F. IOS Press, Amsterdam (2009)
Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: SAC 2009, pp. 615–622. ACM, New York (2009)
Leino, K.R.M., Saxe, J.B., Stata, R.: Checking Java programs via guarded commands. FTfJP 1999. Tech. Rep. 251, Fernuniversität Hagen (May 1999)
Manzano, M.: Extensions of First-Order Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1996)
McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 197–216. Springer, Heidelberg (2002)
McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress 62, pp. 21–28. North-Holland, Amsterdam (1962)
Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reason. 40(1), 35–60 (2008)
Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. TOPLAS 21(3), 527–568 (1999)
Pierce, B.C.: Types and Programming Languages. The MIT Press, Cambridge (2002)
Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitationsschrift, Technische Universität München (1997)
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
Leino, K.R.M., Rümmer, P. (2010). A Polymorphic Intermediate Verification Language: Design and Logical Encoding. In: Esparza, J., Majumdar, R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010. Lecture Notes in Computer Science, vol 6015. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12002-2_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-12002-2_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12001-5
Online ISBN: 978-3-642-12002-2
eBook Packages: Computer ScienceComputer Science (R0)