Thomas Ball
Todd Millstein
Abstract
Model checking has been widely successful in validating and debugging designs in the hardware and protocol domains. However, state-space explosion limits the applicability of model checking tools, so model checkers typically operate on abstractions of systems.
Recently, there has been significant interest in applying model checking to software. For infinite-state systems like software, abstraction is even more critical. Techniques for abstracting software are a prerequisite to making software model checking a reality.
We present the first algorithm to automatically construct a predicate abstraction of programs written in am industrial programming language such as C, and its implementation in a tool -- C2BP. The C2BP tool is part of the SLAM toolkit, which uses a combination of predicate abstraction, model checking, symbolic reasoning, and iterative refinement to statically check temporal safety properties of programs.
Predicate abstraction of software has many applications, including detecting program errors, synthesizing program invariants, and improving the precision of program analyses through predicate sensitivity. We discuss our experience applying the C2BP predicate abstraction tool to a variety of problems, ranging from checking that list-manipulating code preserves heap invariants to finding errors in Windows NT device drivers.
- G. Ammons and J. R. Larus. Improving data-flow analysis with path profiles. In PLDI 98: Programming Language Design and Implementation, pages 72--84. ACM, 1998. Google Scholar
Digital Library
- T. Ball, S. Chaki, and S. K. Rajamani. Parameterized verification of multithreaded software libraries. In TACAS 01: Tools and Algorithms/or Construction and Analysis of Systems, LNCS 2031. Springer-Verlag, 2001. Google ScholarDigital Library
- T. Ball, T. Millstein, and S. K. Rajamani. Polymorphic predicate abstraction. Technical Report MSR Technical Report 2001-10, Microsoft Research, 2000.Google Scholar
- T. Ball, A. Podelski, and S. K. Rajamani. Boolean and cartesian abstractions for model checking C programs. In TA GAS OI: Tools and Algorithms for Construction and Analysis of Systems, LNCS 2031. Springer-Verlag, 2001. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for Boolean programs. In SPIN 00: SPIN Workshop, IJNCS 1885, pages 113--130. Springer-Verlag, 2000. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN 2001: SPIN Workshop, LNCS 2057, May 2001. Google ScholarDigital Library
- D. Blei and et al. Vampyre: A proof generating theorem prover -- http://www.eecs.berkeley.edu/" rupak/vampyre.Google Scholar
- R. Bodik and S. Anik. Path-sensitive value-flow analysis. in POPL 98: Principles o/Programming Languages, pages 237--251. ACM, 1998. Google ScholarDigital Library
- R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677--691, 1986. Google ScholarDigital Library
- J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera : Extracting finitestate models from Java source code. In ICSE'00: Software Engineering, 2000. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In POPL'77: Principles of Programming Languages, pages 238--252. ACM, 1977. Google ScholarDigital Library
- M. Das. Unification-based pointer analysis with directional assignments. In PLDI'00: Programming Language Design and Implementation, pages 35--46. ACM, 2000. Google ScholarDigital Library
- S. Das, D. L. Dill, and S. Park. Experience with predicate abstraction. In CAV 00: Computer-Aided Verification, LNCS 1633, pages 160--171. Springer-Verlag, 1999. Google ScholarDigital Library
- R. DeLine and M. F~hndrich. Enforcing high-level protocols in low-level software. In PLDI'01: Programming Language Design and Implementation. ACM, 2001. Google ScholarDigital Library
- D. Detlefs, G. Nelson, and J. Saxe. Simplify theorem prover - http://research.compaq.com/src/esc/simplify.html.Google Scholar
- E. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. Google ScholarDigital Library
- M. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, Robby, W. Visser, and H. Zheng. Tool-supported program abstraction for finite-state verification. In ICSE'01: Software Engineering (to appear), 2001. Google ScholarDigital Library
- C. Flanagan, R. Joshi, and K. R. M. Leino. Annotation inference for modular checkers. Information Processing Letters (to appear), 2001. Google ScholarDigital Library
- S. Graf and H. Saídi. Construction of abstract state graphs with PVS. In CAV'97: Computer-aided Verification, LNCS 1254, pages 72--83. Springer-Verlag, 1997. Google ScholarDigital Library
- D. Gries. The Science of Programming. Springer-Verlag, 1981. Google ScholarDigital Library
- N. Heintze. Set-based analysis of ML programs. In LFP'94: LISP and Functional Programming, pages 306--317. ACM, 1994. Google ScholarDigital Library
- S. Ishtiaq and P. O'Hearn. BI as an assertion language for mutable data structures. In POPL'01: Principles of Programming Languages, pages 14--26. ACM, 2001. Google ScholarDigital Library
- L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125--143, 1977. Google ScholarDigital Library
- W. Landi, B. G. Ryder, and S. Zhang. Interprocedural side effect analysis with pointer aliasing. In PLDI'93: Programming Language Design and Implementation, pages 56--67. ACM, 1993. 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
- G. 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
- 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
- J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millenial Perspectives in Computer Science, pages 303--321. Palgrave, 2001.Google Scholar
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In POPL'99: Principles of Programming Languages, pages 105--118. ACM, 1999. Google ScholarDigital Library
- M. Sharir and A. Pnueli. Two approaches to iaterprocedural data dalow analysis. In Program Flow Analysis: Theory and Applications, pages 189--233. Prentice-Hall, 1981.Google Scholar
- N. Suzuki and K. Ishihata. Implementation of an array bound checker. In POPL'77: Principles of Programming Languages, pages 132--143. ACM, 1977. Google ScholarDigital Library
- Z. Xu, B. P. Miller, and T. Reps. Safety checking of machine code. In PLDI'00: Programming Language Design and Implementation, pages 70--82. ACM 2000. Google ScholarDigital Library
Index Terms
- Automatic predicate abstraction of C programs
Recommendations
Automatic predicate abstraction of C programs
Model checking has been widely successful in validating and debugging designs in the hardware and protocol domains. However, state-space explosion limits the applicability of model checking tools, so model checkers typically operate on abstractions of ...
Automatic predicate abstraction of C programs
PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementationModel checking has been widely successful in validating and debugging designs in the hardware and protocol domains. However, state-space explosion limits the applicability of model checking tools, so model checkers typically operate on abstractions of ...
Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesPredicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Comments