Bebop: A Symbolic Model Checker for Boolean Programs

By Thomas Ball, Sriram K. Rajamani. SPIN, 2000

419 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/b9b32c3e5645010f8d5170e702946ca9d052f872

How researchers see this paper

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

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

Thorough static analysis of device drivers (2006, background): “This harness leads to fewer false errors being reported but results in increased analysis times.”
Software model checking (2009, positive): “A tool called Bebop then implemented a symbolic model checker for (recursive) Boolean programs [Ball and Rajamani 2000].”
The SLAM Toolkit (2001, methodology): “…P into a boolean program 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 re(cid:12)ne the boolean program, by analyzing the feasibility of paths in the C…”
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft (2004, methodology): “After we had written the technical report we started implementing the Check step in the Bebop model checker [ BR00a ,BR01a].”
Adding nesting structure to words (2006, methodology): “The resulting models hence have finite-state but stack-based control flow (see Boolean programs [8] and recursive state machines [1] as concrete instances of pushdown models of programs).”
WYSINWYX: What you see is not what you eXecute (2010, methodology): “DDA/x86 can analyze stripped device-driver executables, and thus provides a capability not found in previous tools for analyzing device drivers [Ball and Rajamani 2000; Henzinger et al. 2002].”
A Temporal Logic of Nested Calls and Returns (2004, methodology): “This problem has been well studied over the last few years leading to eÆcient implementations and applications to program analysis as well as model checking of C or Java programs [24, 2, 13, 10].”
Boolean and Cartesian abstraction for model checking C programs (2001, methodology): “For more detail on Phase (2), see [2].”
Visibly pushdown languages (2004, background): “The problem of checking regular requirements of pushdown models has been extensively studied in recent years leading to efficient implementations and applications to program analysis [21, 5, 6, 3, 15, 14, 13].”
The pointer assertion logic engine (2000, background): “Model checkers such as Bebop [2] and Bandera [9] ab- stract away the heap and only verify properties of control flow.”
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].”
Analysis of Recursive Game Graphs Using Data Flow Equations (2004, background): “A partial list of references includes [BS92,Wal96,BEM97,Rep98,EHRS00, BR00 ,AEY01,BGR01,Cac02a,CDT02].”
Automatically validating temporal safety properties of interfaces (2001, methodology): “The syntax and semantics of boolean program was de ned in [3].”
A Survey of Automated Techniques for Formal Software Verification (2008, methodology): “Some software model checkers, such as an early version of the Java Pathfinder (JPF), translate Java code to PROMELA and use SPIN for model checking [105].”
From symptom to cause: localizing errors in counterexample traces (2003, methodology): “If not, one must first construct a suitable abstraction of the program, such as a boolean program [2].”
Bugs as deviant behavior: a general approach to inferring errors in systems code (2001, background): “The SLAM project [2] is a promising variation on this approach.”