Hostname: page-component-78c5997874-j824f Total loading time: 0 Render date: 2024-11-09T14:50:02.190Z Has data issue: false hasContentIssue false

Automatically inferring loop invariants via algorithmic learning

Published online by Cambridge University Press:  17 December 2014

YUNGBUM JUNG
Affiliation:
Program Analysis Department, Fasoo, Seoul, Republic of Korea
SOONHO KONG
Affiliation:
School of Computer Science, Carnegie Mellon University, Pittsburgh, United States Email: [email protected]
CRISTINA DAVID
Affiliation:
Department of Computer Science School of Computing, National University of Singapore, Singapore
BOW-YAW WANG
Affiliation:
INRIA and Institute of Information Science, Academia Sinica, Taipei, Taiwan
KWANGKEUN YI
Affiliation:
School of Computer Science and Engineering, Seoul National University, Seoul, Republic of Korea

Abstract

By combining algorithmic learning, decision procedures, predicate abstraction and simple templates for quantified formulae, we present an automated technique for finding loop invariants. Theoretically, this technique can find arbitrary first-order invariants (modulo a fixed set of atomic propositions and an underlying satisfiability modulo theories solver) in the form of the given template and exploit the flexibility in invariants by a simple randomized mechanism. In our study, the proposed technique was able to find quantified invariants for loops from the Linux source and other realistic programs. Our contribution is a simpler technique than the previous works yet with a reasonable derivation power.

Type
Paper
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

This work was supported by the Engineering Research Center of Excellence Program of Korea Ministry of Education, Science and Technology (MEST) / National Research Foundation of Korea (NRF) (Grant 2011-0000971), the National Science Foundation (award no. CNS0926181), the National Science Council of Taiwan projects No. NSC97-2221-E-001-003-MY3, NSC97-2221-E-001-006-MY3, the FORMES Project within LIAMA Consortium, and the French ANR project SIVES ANR-08-BLAN-0326-01. This research was sponsored in part by the National Science Foundation (award no. CNS0926181) and by Republic of Korea Dual Use Program Cooperation Center (DUPC) of Agency for Defense Development (ADD).

References

Alur, R., Cerný, P., Madhusudan, P. and Nam, W. (2005a) Synthesis of interface specifications for java classes. In: POPL, ACM 98109.Google Scholar
Alur, R., Madhusudan, P. and Nam, W. (2005b) Symbolic compositional verification by learning assumptions. In: CAV. Springer Lecture Notes in Computer Science 3576 548562.CrossRefGoogle Scholar
Bertot, Y. and Castéran, P. (2004) Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, Springer Verlag.CrossRefGoogle Scholar
Bshouty, N. H. (1995) Exact learning boolean functions via the monotone theory. Information and Computation 123 146153.Google Scholar
Chen, Y.-F., Farzan, A., Clarke, E. M., Tsay, Y.-K. and Wang, B.-Y. (2009) Learning minimal separating DFA's for compositional verification. In: TACAS. Springer Lecture Notes in Computer Science 5505 3145.CrossRefGoogle Scholar
Cobleigh, J. M., Giannakopoulou, D. and Păsăreanu, C. S. (2003) Learning assumptions for compositional verification. In: TACAS. Springer Lecture Notes in Computer Science 2619 331346.Google Scholar
Dutetre, B. and de Moura, L. D. (2006) The Yices SMT solver, Technical report, SRI International. Available at: http://yices.csl.sri.com/tool-paper.pdfGoogle Scholar
Flanagan, C. and Qadeer, S. (2002) Predicate abstraction for software verification. In: POPL, ACM 191202.Google Scholar
Ge, Y. and Moura, L. (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: CAV. Springer-Verlag Lecture Notes in Computer Science 5643 306320.Google Scholar
Gulwani, S., McCloskey, B. and Tiwari, A. (2008a) Lifting abstract interpreters to quantified logical domains. In: POPL, ACM 235246.Google Scholar
Gulwani, S., Srivastava, S. and Venkatesan, R. (2008b) Program analysis as constraint solving. In: PLDI, ACM 281292.Google Scholar
Gulwani, S., Srivastava, S. and Venkatesan, R. (2009) Constraint-based invariant inference over predicate abstraction. In: VMCAI. Springer Lecture Notes in Computer Science 5403 120135.Google Scholar
Gupta, A., McMillan, K. L. and Fu, Z. (2007) Automated assumption generation for compositional verification. In: CAV. Springer Lecture Notes in Computer Science 4590 420432.Google Scholar
Gupta, A. and Rybalchenko, A. (2009) Invgen: An efficient invariant generator. In: CAV. Springer Lecture Notes in Computer Science 5643 634640.CrossRefGoogle Scholar
Halbwachs, N. and Péron, M. (2008) Discovering properties about arrays in simple programs. In: PLDI 339348.Google Scholar
Henzinger, T. A., Hottelier, T., Kovács, L. and Voronkov, A. (2010) Invariant and type inference for matrices. In: VMCAI 163179.Google Scholar
Jhala, R. and McMillan, K. L. (2007) Array abstractions from proofs. In: CAV. Springer Lecture Notes in Computer Science 4590 193206.CrossRefGoogle Scholar
Jung, Y., Kong, S., Wang, B.-Y. and Yi, K. (2010) Deriving invariants in propositional logic by algorithmic learning, decision procedure and predicate abstraction. In: VMCAI. Springer Lecture Notes in Computer Science 5944 180196.CrossRefGoogle Scholar
Jung, Y., Lee, W., Wang, B.-Y. and Yi, K. (2011) Predicate generation for learning-based quantifier-free loop invariant inference. In: TACAS 205219.Google Scholar
Kong, S., Jung, Y., David, C., Wang, B.-Y. and Yi, K. (2010) Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: The 8th ASIAN Symposium on Programming Languages and Systems (APLAS'10) 328343.Google Scholar
Kovács, L. and Voronkov, A. (2009) Finding loop invariants for programs over arrays using a theorem prover. In: FASE. Springer Lecture Notes in Computer Science 5503 470485.Google Scholar
Kroening, D. and Strichman, O. (2008) Decision Procedures An Algorithmic Point of View, EATCS, Springer.Google Scholar
Lahiri, S. K., Bryant, R. E. and Bryant, A. E. (2004) Constructing quantified invariants via predicate abstraction. In: VMCAI. Springer Lecture Notes in Computer Science 2937 267281.Google Scholar
McMillan, K. L. (2008) Quantified invariant generation using an interpolating saturation prover. In: TACAS. Springer Lecture Notes in Computer Science 4693 413427.CrossRefGoogle Scholar
Nipkow, T., Paulson, L. C. and Wenzel, M. (2002) Isabelle/HOL — A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, volume 2283.Google Scholar
Srivastava, S. and Gulwani, S. (2009) Program verification using templates over predicate abstraction. In: PLDI, ACM 223234.Google Scholar
Srivastava, S., Gulwani, S. and Foster, J. S. (2009) Vs3: Smt solvers for program verification. In: CAV '09: Proceedings of Computer Aided Verification 702708.Google Scholar