ABSTRACT
The success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is parsimonious if at each control location, it specifies only relationships between current values of variables, and only those which are required for proving correctness. Previous methods for automatically refining predicate abstractions until sufficient precision is obtained do not systematically construct parsimonious abstractions: predicates usually contain symbolic variables, and are added heuristically and often uniformly to many or all control locations at once. We use Craig interpolation to efficiently construct, from a given abstract error trace which cannot be concretized, a parsominous abstraction that removes the trace. At each location of the trace, we infer the relevant predicates as an interpolant between the two formulas that define the past and the future segment of the trace. Each interpolant is a relationship between current values of program variables, and is relevant only at that particular program location. It can be found by a linear scan of the proof of infeasibility of the trace.We develop our method for programs with arithmetic and pointer expressions, and call-by-value function calls. For function calls, Craig interpolation offers a systematic way of generating relevant predicates that contain only the local variables of the function and the values of the formal parameters when the function was called. We have extended our model checker Blast with predicate discovery by Craig interpolation, and applied it successfully to C programs with more than 130,000 lines of code, which was not possible with approaches that build less parsimonious abstractions.
- T. Ball, T. Millstein, and S.K. Rajamani. Polymorphic predicate abstraction. ACM Transactions on Programming Languages and Systems, 2003. Google ScholarDigital Library
- T. Ball and S.K. Rajamani. Personal communication.Google Scholar
- T. Ball and S.K. Rajamani. Generating abstract explanations of spurious counterexamples in C programs. Technical Report MSR-TR-2002-09, Microsoft Research, 2002.Google Scholar
- T. Ball and S.K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL 02: Principles of Programming Languages, pages 1--3. ACM, 2002. Google ScholarDigital Library
- R. Bodik, R. Gupta, and M.L. Soffa. Refining dataflow information using infeasible paths. In FSE 97: Foundations of Software Engineering, LNCS 1301, pages 361--377. Springer, 1997. Google ScholarDigital Library
- W.R. Bush, J.D. Pincus, and D.J. Sielaff. A static analyzer for finding dynamic programming errors. Software Practice and Experience, 30:775--802, 2000. Google ScholarDigital Library
- S. Chaki, E.M. Clarke, A. Groce, and O. Strichman. Predicate abstraction with minimum predicates. In CHARME 03: Correct Hardware Design and Verification, LNCS 2860, pages 19--34. Springer, 2003.Google ScholarCross Ref
- E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV 00: Computer-Aided Verification, LNCS 1855, pages 154--169. Springer, 2000. Google ScholarDigital Library
- W. Craig. Linear reasoning. J. Symbolic Logic, 22:250--268, 1957.Google ScholarCross Ref
- R. Cytron, J. Ferrante, B.K. Rosen, M.N. Wegman, and F.K. Zadek. Efficiently computing static single assignment form and the program dependence graph. ACM Transactions on Programming Languages and Systems, 13:451--490, 1991. Google ScholarDigital Library
- M. Das, S. Lerner, and M. Seigle. ESP: path-sensitive program verification in polynomial time. In PLDI 02: Programming Language Design and Implementation, pages 57--68. ACM, 2002. Google ScholarDigital Library
- C. Flanagan. Automatic software model checking using CLP. In ESOP 03: European Symposium on Programming, LNCS 2618, pages 189--203. Springer, 2003. Google ScholarDigital Library
- C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata. Extended static checking for Java. In PLDI 02: Programming Language Design and Implementation, pages 234--245. ACM, 2002. Google ScholarDigital Library
- C. Flanagan and J.B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In POPL 01: Principles of Programming Languages, pages 193--205. ACM, 2001. Google ScholarDigital Library
- J.S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In PLDI 02: Programming Language Design and Implementation, pages 1--12. ACM, 2002. Google ScholarDigital Library
- D. Gries. The Science of Programming. Springer, 1981. Google ScholarCross Ref
- T.A. Henzinger, R. Jhala, R. Majumdar, G.C. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In CAV 02: Computer-Aided Verification, LNCS 2404, pages 526--538. Springer, 2002. Google ScholarDigital Library
- T.A. Henzinger, R. Jhala, R. Majumdar, and M.A.A. Sanvido. Extreme model checking. In International Symposium on Verification, LNCS. Springer, 2003.Google ScholarCross Ref
- T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL 02: Principles of Programming Languages, pages 58--70. ACM, 2002. Google ScholarDigital Library
- J. Krajicek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symbolic Logic, 62:457--486, 1997.Google ScholarCross Ref
- J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In Proc. Symposia in Applied Mathematics. American Mathematical Society, 1967.Google ScholarCross Ref
- K.L. McMillan. Interpolation and SAT-based model checking. In CAV 03: Computer-Aided Verification, LNCS 2725, pages 1--13. Springer, 2003.Google ScholarCross Ref
- J.C. Mitchell. Foundations for Programming Languages. MIT Press, 1996. Google ScholarDigital Library
- J. M. Morris. A general axiom of assignment. In Theoretical Foundations of Programming Methodology, Lecture Notes of an International Summer School, pages 25--34. D. Reidel Publishing Company, 1982.Google ScholarCross Ref
- M. Musuvathi, D.Y.W. Park, A. Chou, D.R. Engler, and D.L. Dill. CMC: A pragmatic approach to model checking real code. In OSDI 02: Operating Systems Design and Implementation. ACM, 2002. Google ScholarDigital Library
- G.C. Necula. Proof carrying code. In POPL 97: Principles of Programming Languages, pages 106--119. ACM, 1997. Google ScholarDigital Library
- G. Nelson. Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center, 1981.Google Scholar
- P. Pudlak. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic, 62:981--998, 1997.Google ScholarCross Ref
- T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL 95: Principles of Programming Languages, pages 49--61. ACM, 1995. Google ScholarDigital Library
Index Terms
- Abstractions from proofs
Recommendations
Abstractions from proofs
POPL '04The success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is parsimonious if at each control location, it specifies only relationships between current ...
Abstractions from proofs
Supplemental issueThe success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is parsimonious if at each control location, it specifies only relationships between current ...
Counterexample-guided predicate abstraction of hybrid systems
Tools and algorithms for the construction and analysis of systems (TACAS 2003)Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the teachability computation techniques for hybrid systems. Given a ...
Comments