Isil Dillig
Skip Abstract Section
Abstract
This paper presents a new method for generating inductive loop invariants that are expressible as boolean combinations of linear integer constraints. The key idea underlying our technique is to perform a backtracking search that combines Hoare-style verification condition generation with a logical abduction procedure based on quantifier elimination to speculate candidate invariants. Starting with true, our method iteratively strengthens loop invariants until they are inductive and strong enough to verify the program. A key feature of our technique is that it is lazy: It only infers those invariants that are necessary for verifying program correctness. Furthermore, our technique can infer arbitrary boolean combinations (including disjunctions) of linear invariants. We have implemented the proposed approach in a tool called HOLA. Our experiments demonstrate that HOLA can infer interesting invariants that are beyond the reach of existing state-of-the-art invariant generation tools.
- Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints among Variables of a Program. In: POPL, ACM (1978) 84--96. Google Scholar
Digital Library
- Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1) (2006) 31--100. Google ScholarDigital Library
- Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, ACM (1979) 269--282. Google ScholarDigital Library
- Karr, M.: Affine relationships among variables of a program. A. I. (1976) 133--151.Google Scholar
- Gupta, A., Rybalchenko, A.: Invgen: An efficient invariant generator. In: Computer Aided Verification, Springer (2009) 634--640. Google ScholarDigital Library
- Colón, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Computer Aided Verification, Springer (2003) 420--432.Google Scholar
- Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: International conference on Model checking software. (2003) 235--239. Google ScholarDigital Library
- Ball, T., Rajamani, S.: The slam toolkit. In: Computer aided verification, Springer (2001) 260--264. Google Scholar
- McMillan, K.: Lazy annotation for program testing and verification. In: Computer Aided Verification, Springer (2010) 104--118. Google ScholarDigital Library
- Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. ACM SIGPLAN Notices 39(1) (2004) 232--244. Google ScholarDigital Library
- McMillan, K.: Interpolation and sat-based model checking. In: Computer Aided Verification, Springer (2003) 1--13.Google ScholarCross Ref
- Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., Stata, R.: Extended static checking for java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation. PLDI '02, New York, NY, USA, ACM (2002) 234--245. Google ScholarDigital Library
- Leino, K.: Dafny: An automatic program verifier for functional correctness. In: Logic for Programming, Artificial Intelligence, and Reasoning, Springer (2010) 348--370. Google ScholarDigital Library
- Barnett, M., yuh Evan Chang, B., Deline, R., Jacobs, B., Leino, K. R.: Boogie: A modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, volume 4111 of Lecture Notes in Computer Science, Springer (2006) 364--387. Google ScholarDigital Library
- Peirce, C.: Collected papers of Charles Sanders Peirce. Belknap Press (1932).Google Scholar
- Dillig, I., Dillig, T., McMillan, K., Aiken, A.: Minimum satisfying assignments for SMT, CAV (2012). Google ScholarDigital Library
- Cooper, D.: Theorem proving in arithmetic without multiplication. Machine Intelligence 7(91-99) (1972) 300.Google Scholar
- Dillig, I., Dillig, T., Aiken, A.: SAIL: Static Analysis Intermediate Language. Stanford University Technical Report.Google Scholar
- Dillig, I., Dillig, T., Aiken, A.: Small formulas for large programs: On-line constraint simplification in scalable static analysis. SAS (2011). Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A.: Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. In: CAV. (2009). Google ScholarDigital Library
- Jeannet, B.: Interproc analyzer for recursive programs with numerical variables. http://pop-art.inrialpes.fr/interproc/interprocweb.cgi.Google Scholar
- Bradley, A.: Understanding IC3. Theory and Applications of Satisfiability Testing - SAT 2012 (2012) 1--14. Google ScholarDigital Library
- Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI. Volume 43., ACM (2008) 281--292. Google ScholarDigital Library
- Jhala, R., McMillan, K.: A practical and complete approach to predicate refinement. Tools and Algorithms for the Construction and Analysis of Systems (2006) 459--473. Google ScholarDigital Library
- Sharma, R., Nori, A., Aiken, A.: Interpolants as classifiers. In: Computer Aided Verification, Springer (2012) 71--87. Google ScholarDigital Library
- Gulavani, B., Rajamani, S.: Counterexample driven refinement for abstract interpretation. Tools and Algorithms for the Construction and Analysis of Systems (2006) 474--488. Google ScholarDigital Library
- Gulwani, S., Jojic, N.: Program verification as probabilistic inference. In: ACM SIGPLAN Notices. Volume 42., ACM (2007) 277--289. Google ScholarDigital Library
- Gulavani, B., Chakraborty, S., Nori, A., Rajamani, S.: Automatically refining abstract interpretations. TACAS (2008) 443--458. Google ScholarDigital Library
- Beyer, D., Henzinger, T. A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. PLDI '07, New York, NY, USA, ACM (2007) 300--309. Google ScholarDigital Library
- Bradley, A. R., Manna, Z.: Property-directed incremental invariant generation. Form. Asp. Comput. 20(4-5) (June 2008) 379--405. Google ScholarCross Ref
- Gulavani, B. S., Henzinger, T. A., Kannan, Y., Nori, A. V., Rajamani, S. K.: Synergy: a new algorithm for property checking. In: Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering. SIGSOFT '06/FSE-14, New York, NY, USA, ACM (2006) 117--127. Google ScholarDigital Library
- http://pub.ist.ac.at/agupta/invgen/: InvGen tool.Google Scholar
- http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.php: NECLABS NECLA verification benchmarks.Google Scholar
- Laviron, V., Logozzo, F.: Subpolyhedra: A (more) scalable approach to infer linear inequalities. In: Verification, Model Checking, and Abstract Interpretation, Springer (2009) 229--244. Google ScholarDigital Library
- Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5) (September 2003) 752--794. Google ScholarDigital Library
- Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Verification, Model Checking, and Abstract Interpretation, Springer (2009) 120--135. Google ScholarDigital Library
- Flanagan, C., Leino, K.: Houdini, an annotation assistant for esc/java. FME 2001: Formal Methods for Increasing Software Productivity (2001) 500--517. Google ScholarDigital Library
- Ernst, M., Perkins, J., Guo, P., McCamant, S., Pacheco, C., Tschantz, M., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Science of Computer Programming 69(1-3) (2007) 35--45. Google ScholarDigital Library
- McMillan, K.: Lazy abstraction with interpolants. In: Computer Aided Verification, Springer (2006) 123--136. Google ScholarDigital Library
- Păsăreanu, C. S., Visser, W.: Verification of java programs using symbolic execution and invariant generation. In: SPIN Workshop on Model Checking Software. Springer (2004) 164--181.Google Scholar
- Bradley, A.: Sat-based model checking without unrolling. In: Verification, Model Checking, and Abstract Interpretation, Springer (2011) 70--87. Google ScholarDigital Library
- Somenzi, F., Bradley, A.: IC3: where monolithic and incremental meet. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD Inc (2011) 3--8. Google ScholarDigital Library
- Calcagno, C., Distefano, D., O'Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. POPL 44(1) (2009) 289--300. Google ScholarDigital Library
- Giacobazzi, R.: Abductive analysis of modular logic programs. In: Proceedings of the 1994 International Symposium on Logic programming, Citeseer (1994) 377--391. Google ScholarDigital Library
- Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, ACM (2008) 235--246. Google ScholarDigital Library
- Calcagno, C., Distefano, D., Vafeiadis, V.: Bi-abductive resource invariant synthesis. In: Proceedings of the 7th Asian Symposium on Programming Languages and Systems. APLAS '09, Berlin, Heidelberg, Springer-Verlag (2009) 259--274. Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference. In: Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation. PLDI '12, New York, NY, USA, ACM (2012) 181--192. Google ScholarDigital Library
- Li, B., Dillig, I., Dillig, T.,McMillan, K., Sagiv, M.: Synthesis of circular compositional program proofs via abduction. In: Proceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS'13, Springer-Verlag (2013) 370--384. Google ScholarDigital Library
- Gulwani, S., Musuvathi, M.: Cover Algorithms. In: ESOP. (2008) 193--207. Google ScholarDigital Library
Index Terms
- Inductive invariant generation via abductive inference
Recommendations
Inductive invariant generation via abductive inference
OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applicationsThis paper presents a new method for generating inductive loop invariants that are expressible as boolean combinations of linear integer constraints. The key idea underlying our technique is to perform a backtracking search that combines Hoare-style ...
Property-directed incremental invariant generation
AbstractA fundamental method of analyzing a system such as a program or a circuit is invariance analysis, in which one proves that an assertion holds on all reachable states. Typically, the proof is performed via induction; however, an assertion, while ...
Simplifying loop invariant generation using splitter predicates
CAV'11: Proceedings of the 23rd international conference on Computer aided verificationWe present a novel static analysis technique that substantially improves the quality of invariants inferred by standard loop invariant generation techniques. Our technique decomposes multi-phase loops, which require disjunctive invariants, into a ...
Comments