Path invariants

Abstract

The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false alarm -the spurious counterexample- as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. There are two advantages to using such path programs as counterexamples for abstraction refinement. First, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. Specifically, we use constraint-based invariant generation to automatically infer invariants of path programs-so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. Unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning.

References

1. T. Ball, A. Podelski, and S. K. Rajamani. Relative completeness of abstraction refinement for software model checking. In Proc. TACAS, LNCS 2280, pp. 158--172. Springer, 2002.
2. T. Ball and S. K. Rajamani. The sc Slam project: Debugging system software via static analysis. In Proc. POPL, pp. 1--3. ACM, 2002.
3. D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Invariant synthesis for combined theories. In Proc. VMCAI, LNCS 4349, pp. 378--394. Springer, 2007.
4. B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In Proc. PLDI, pp. 196--207. ACM, 2003.
5. A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability. In Proc. CAV, LNCS 3576, pp. 491--504. Springer, 2005.
6. A. R. Bradley, Z. Manna, and H. B. Sipma. What's decidable about arrays? In Proc. VMCAI, LNCS 3855, pp. 427--442. Springer, 2006.
7. S. Chaki, E. M. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. IEEE Trans. Software Eng., 30:388--402, 2004.
8. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Proc. CAV, LNCS 1855, pp. 154--169. Springer, 2000.
9. M. Colóp;n, S. Sankaranarayanan, and H. B. Sipma. Linear invariant generation using non-linear constraint solving. In Proc. CAV, LNCS 2725, pp. 420--432. Springer, 2003.
10. P. Cousot. Partial completeness of abstract fixpoint checking. In Proc. SARA, LNCS 1864, pp. 1--15. Springer, 2000.
11. P. Cousot. Verification by abstract interpretation. In Verification: Theory and Practice, LNCS 2772, pp. 243--268. Springer, 2003.
12. P. Cousot. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In Proc. VMCAI, LNCS 3385, pp. 1--24. Springer, 2005.
13. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In Proc. POPL, pp. 238--252. ACM, 1977.
14. P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In Proc. PLILP, LNCS 631, pp. 269--295. Springer, 1992.
15. P. Cousot and N.l Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. POPL, pp. 84--96, 1978.
16. S. Das, D. L. Dill, and S. Park. Experience with predicate abstraction. In Proc. CAV, LNCS 1633, pp. 160--171. Springer, 1999.
17. J. Esparza, S. Kiefer, and S. Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. In Proc. TACAS, LNCS 3920, pp. 489--503. Springer, 2006.
18. C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proc. PLDI, pp. 234--245. ACM, 2002.
19. C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In Proc. POPL, pp. 191--202. ACM, 2002.
20. R. W. Floyd. Assigning meanings to programs. In Mathematical Aspects of Computer Science, pp. 19--32. AMS, 1967.
21. D. Gopan, T. W. Reps, and M. Sagiv. A framework for numeric analysis of array operations. In Proc. POPL, pp. 338--350. ACM, 2005.
22. S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In Proc. CAV, LNCS 1254, pp. 72--83. Springer, 1997.
23. S. Gulwani and N. Jojic. Program verification as probabilistic inference. In Proc. POPL, pp. 277--289. ACM, 2007.
24. S.Gulwani and A.Tiwari. Combining abstract interpreters. In Proc. PLDI, pp. 376--386. ACM, 2006.
25. T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In Proc. POPL, pp. 232--244. ACM, 2004.
26. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proc. POPL, pp. 58--70. ACM, 2002.
27. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12:576--580, 1969.
28. F. Ivancic, Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. sc F-Soft: Software verification platform. In Proc. CAV, LNCS 3576, pp. 301--306. Springer, 2005.
29. R. Jhala and K. L. McMillan. A practical and complete approach to predicate refinement. In Proc. TACAS, LNCS 3920, pp. 459--473. Springer, 2006.
30. D. Kapur. Automatically generating loop invariants using quantifier elimination. Technical Report 05431 (it Deduction and Applications), IBFI Schloss Dagstuhl, 2006.
31. D. Kapur and C. Zarba. A reduction approach to decision procedures. Technical Report TR-CS-2005-44, University of New Mexico, 2005.
32. M. Karr. Affine relationships among variables of a program. Acta Inf., 6:133--151, 1976.
33. J. C. King. Symbolic execution and program testing. Commun. ACM, 19:385--394, 1976.
34. S. K. Lahiri and R. E. Bryant. Indexed predicate discovery for unbounded system verification. In Proc. CAV, LNCS 3114, pp. 135--147. Springer, 2004.
35. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995.
36. LMauborgne and X. Rival. Trace partitioning in abstract interpretation based static analyzers. In Proc. ESOP, LNCS 3444, pp. 5--20. Springer, 2005.
37. K. L. McMillan. Lazy abstraction with interpolants. In Proc. CAV, LNCS 4144, pp. 123--136. Springer, 2006.
38. AMiné. The octagon abstract domain. Higher-Order and Symbolic Comp., 19:31--100, 2006.
39. M. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst., 24:217--298, 2002.
40. S. Sankaranarayanan, F. Ivancic, I. Shlyakhter, and A. Gupta. Static analysis in disjunctive numerical domains. In Proc. SAS, LNCS 4134, pp. 3--17. Springer, 2006.
41. S. Sankaranarayanan, H. B. Sipma, and Z. Manna. Constraint-based linear-relations analysis. In Proc. SAS, LNCS 3148, pp. 53--68. Springer, 2004.
42. S. Sankaranarayanan, H. B. Sipma, and Z. Manna. Non-linear loop invariant generation using Gröbner bases. In Proc. POPL, pp. 318--329. ACM, 2004.
43. S. Sankaranarayanan, H. B. Sipma, and Z. Manna. Scalable analysis of linear systems using mathematical programming. In Proc. VMCAI, LNCS 3385, pp. 25--41. Springer, 2005.
44. V. Sofronie-Stokkermans. Hierarchic reasoning in local theory extensions. In Proc. CADE, LNCS 3632, pp. 219--234. Springer, 2005.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program verification