Boolean and Cartesian abstraction for model checking C programs

By Thomas Ball, Andreas Podelski, Sriram K. Rajamani. International Journal on Software Tools for Technology Transfer (STTT), 2001

379 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/1afe9ab5939d96f86c9a6bb4bb61f697227ac23c

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Principles of model checking (2008, methodology): “The automated generation of abstract models amenable to model checking from programs written in programming languages such as C, C++, or Java has been pursued, for instance, by Godefroid [170], Dwyer, Hatcliff, and coworkers [193], at Microsoft Research by Ball, Podelski, and Rajamani [33] and at NA”
Model checking programs (2000, methodology): “The aim of this work is to do reachability analysis for large sequential C programs, with specific application to device drivers (Ball and Rajamani, 2000b; Ball et al., 2001b).”
Automatic predicate abstraction of C programs (2001, methodology): “We improve precision by using disjunctive completion and focus operations, both of which are implemented in Bebop using BDDs [4].”
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft (2004, background): “Andreas’ work greatly aided us in understanding the theoretical capabilities and limitations of the SLAM process [ BPR01 ,BPR02].”
Lazy Abstraction with Interpolants (2006, methodology): “Because of this, weak approximations are typically used, such as the Cartesian or “Boolean Programs” approximations [1], with the associated need for refinement in case of failures.”
A Survey of Automated Techniques for Formal Software Verification (2008, background): “Intuitively, if we could search deep enough, we could guarantee that we have examined all the relevant behaviors of the model and that searching any deeper only exhibits states that we have explored already.”
Software model checking (2009, unknown): “This method was popularized by Slam which uses predicate abstraction [Agerwala and Misra 1978; Graf and Sa¨ıdi 1997] to abstract C programs into boolean programs [Ball et al. 2001] which are subsequently model checked us-ing Bebop as described above.”
Modular verification of software components in C (2003, background): “However, due to compositionality, we can afford to invest more computing power into computing abstractions, and are therefore able to improve on Cartesian abstraction [12].”
Automatically validating temporal safety properties of interfaces (2001, methodology): “C2bp, a tool that transforms a C program P into a boolean program BP(P;E) with respect to a set of predicates E over the state space of P [1, 2];”
The SLAM Toolkit (2001, methodology): “BP(P;E) with respect to a set of predicates E over P [1, 2 ]; { Bebop, a tool for model checking boolean programs [3], and { Newton, a tool that discovers additional predicates to rene the boolean program, by analyzing the feasibility of paths in the C program.”
Lazy abstraction (2002, background): “In particular, p"~'Tst(r, l) is not the smallest set containing post(r, l) expressible in terms of the support predicates - - indeed, we lose information in constructing a Cartesian abstraction [4, 20].”