Abstract
Predicate abstraction is an effective technique for scaling Software Model Checking to real programs. Traditionally, predicate abstraction abstracts each basic block of a program \(\mathcal{P}\) to construct a small finite abstract model – a Boolean program BP, whose state-transition relation is over some chosen (finite) set of predicates. This is called Small-Block Encoding (SBE). A recent advancement is Large-Block Encoding (LBE) where abstraction is applied to a “summarized” program so that the abstract transitions of BP correspond to loop-free fragments of \(\mathcal{P}\). In this paper, we expand on the original notion of LBE to promote flexibility. We explore and describe efficient ways to perform CEGAR bottleneck operations: generating and solving predicate abstraction queries (PAQs). We make the following contributions. First, we define a general notion of program summarization based on loop cutsets. Second, we give a linear time algorithm to construct PAQs for a loop-free fragment of a program. Third, we compare two approaches to solving PAQs: a classical AllSAT-based one, and a new one based on Linear Decision Diagrams (LDDs). The approaches are evaluated on a large benchmark from open-source software. Our results show that the new LDD-based approach significantly outperforms (and complements) the AllSAT one.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001)
Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software Model Checking via Large-Block Encoding. In: FMCAD 2009 (2009)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123. Springer, Heidelberg (2008)
Cavada, R., Cimatti, A., Franzén, A., Kalyanasundaram, K., Roveri, M., Shyamasundar, R.K.: Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. In: FMCAD 2007 (2007)
Chaki, S., Gurfinkel, A., Strichman, O.: Decision Diagrams for Linear Arithmetic. In: FMCAD 2009 (2009)
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate Abstraction of ANSI-C Programs using SAT. FMSD 25(2-3) (2004)
Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. TOPLAS 13(4) (1991)
Das, S., Dill, D.: Successive Approximation of Abstract Transition Relations. In: LICS 2001, pp. 51–60 (2001)
Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: POPL 2002, pp. 58–70 (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions From Proofs. In: POPL 2004 (2004)
Karp, R.M.: Reducibility Among Combinatorial Problems. In: Complexity of Computer Computations, pp. 85–103 (1972)
Kroening, D., Sharygina, N.: Approximating Predicate Images for Bit-Vector Logic. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 242–256. Springer, Heidelberg (2006)
Lahiri, S.K., Ball, T., Cook, B.: Predicate Abstraction via Symbolic Decision Procedures. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 24–38. Springer, Heidelberg (2005)
Lahiri, S.K., Bryant, R.E., Cook, B.: A Symbolic Approach to Predicate Abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 141–153. Springer, Heidelberg (2003)
Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT Techniques for Fast Predicate Abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 424–437. Springer, Heidelberg (2006)
Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: CGO 2004 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gurfinkel, A., Chaki, S., Sapra, S. (2011). Efficient Predicate Abstraction of Program Summaries. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds) NASA Formal Methods. NFM 2011. Lecture Notes in Computer Science, vol 6617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-20398-5_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20397-8
Online ISBN: 978-3-642-20398-5
eBook Packages: Computer ScienceComputer Science (R0)