Competent predicate abstraction in model checking
Tóm tắt
The paper presents a new approach to computing the abstract state and a maximum weight heuristic method for finding the shortest counter-example in verification of imperative programs. The strategy is incorporated in a verification system based on the counterexample-guided abstraction refinement method. The proposed method slashes both the size of the abstract state space and the number of invokes of a decision procedure. A number of benchmarks are employed to evaluate the effectiveness of the approach.
Tài liệu tham khảo
Graf S, Saidi H. Construction of abstract state graphs with PVS. In: CAV97, Haifa, Isreal, 1997, 1254: 72–83
Das S, Dill D, Park P. Experience with predicate abstraction. CAV99, 1999, 1166: 187–201
Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge, MA: The MIT Press, 1999. 122–124
Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fix points. In: POPL77, Los Angeles, California, 1977. 238–252
Loiseaux C, Graf S, Sifakis J, et al. Property preserving abstractions for the verification of concurrent systems. J FMSD, 1995, 6: 11–44
Ranzato F. On the completeness of model checking. ESOP’2001, 2001, 2028: 137–154
Clarke E M, Grumberg O, Jha S, et al. Counterexample-guided abstraction refinement. CAV00, 2000, 1855: 154–169
Henzinger T A, Jhala R, Majumdar R, et al. Lazy abstraction. POPL 2002, 2002, 37: 58–70
Ball T, Majumdar R, Millstein T, et al. Automatic predicate abstraction of C programs. PLDI01, 2001, 36: 203–213
Ball T, Cook B, Das S, et al. Refining approximations in software predicate abstraction. TACAS04, 2004, 2988: 388–403
Henzinger T A, Majumdar R. A classification of symbolic transition systems. STACS00, 2000, 1770: 13–34
Schmidt D A. Underapproximating predicate transformers. SAS06, 2006, 4134: 127–143
Dijkstra E W. A Discipline of Programming. Upper Saddle River, NJ: Prentice Hall 1976. 32–35
Huth M, Ryan M. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge: Cambridge University Press, 2001. 189–193
Fitting M. Kleene’s logic, generalized. J LC, 1991, 1: 797–810
Beyer D, Chlipala A J, Henzinger T A, et al. The blast query language for software verification. SAS04, 2004, 3148: 2–18
Rosenblum D S. A practical approach to programming with assertions. J IEEE TSE, 1995, 21: 265–265
McMillan K L. Application of craig interpolants in model checking. APN05, 2005, 3440: 1–12
McMillan K L. An interpolating theorem prover. J TCS, 2005, 345: 101–121
Li L, He K D, Li J, et al. Jckecher: A software model checker. http://code.google.com/p/jchecker/.
Blei D, Harrelson C, Jhala R, et al. Vampyre: a proof generating theorem prover. http://www.eecs.berkeley.edu/~rupak/Vampyre.
Henzinger T A, Majumdar R, Beyer D, et al. BLAST: Berkeley lazy abstraction software verification tool. http://mtc.epfl.ch/software-tools/blast/