Automatic predicate abstraction of C programs

By Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2001

676 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Hardware and Architecture

View Paper: https://www.semanticscholar.org/paper/29a67d1a56c463b7d2524d231330d984aa28af19

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 Hardware and Architecture

Citations in the corpus

Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution (2005, neutral): “Recently, tools such as S LAM [2,4] and Blast [7,17] were adapted for test generation.”
Introduction to Embedded Systems - A Cyber-Physical Systems Approach (2013, background): “4: Consider the multithreaded program given below (adapted from Ball et al. (2001)).”
Secure two-party computations in ANSI C (2012, methodology): “As explained above, CBMC reads a C program f containing assertions along with a bound k, and generates a Boolean constraint Bf in CNF such that the satisfying assignments of Cf encode program traces of size at most k that violate the assertions.”
Effective typestate verification in the presence of aliasing (2006, positive): “RELATED WORK Many existing veri.cation frameworks [Das et al. 2002; Ball et al. 2001; Corbett et al. 2000] use a two-phased approach, performing points-to analysis as a preceding phase, followed by typestate checking.”
A Survey of Automated Techniques for Formal Software Verification (2008, neutral): “" SLAM comprises the predicate abstraction tool C2BP [11], [12], the BDD-based model checker BEBOP [14] for Boolean programs [15], and the simulation and refinement tool NEWTON [13].”
Modular verification of software components in C (2003, background): “Given any C expression el and a normal C assignment s, we define the weakest precondition of el with respect to s in the same way as [11] and denote it by l'V79(s, el).”
Boolean and Cartesian abstraction for model checking C programs (2001, methodology): “Continuing Example 3 for the general version of the program with n ≥ 2 Boolean variables, we have post#b·c·∨·[1,2]({〈∗, ∗, ∗, .”
Thorough static analysis of device drivers (2006, background): “This harness leads to fewer false errors being reported but results in increased analysis times.”
A static analyzer for large safety-critical software (2003, methodology): “Moreover most implementations incorporate an automatic refinement process by success and failure [2, 21] whereas we successively refined our abstract domains manually, by experimentation.”
Software Verification with BLAST (2003, background): “Our handling of C features follows that of [1].”
Probabilistic programming (2014, neutral): “We note that the statement observe(x) is very related to the statement assume(x) used in program verification literature [2, 15, 42].”
Termination proofs for systems code (2006, methodology): “SDV currently uses the SLAM software model checker [2] to prove temporal safety properties of device drivers.”
Adding nesting structure to words (2006, methodology): “In the context of software verification, a popular paradigm to verification is through data abstraction, where the data in a program is abstracted using a finite set of boolean variables that stand for predicates on the data-space [7, 10].”
From symptom to cause: localizing errors in counterexample traces (2003, methodology): “The algorithm fails to localize this cause since it belongs to a portion of t1 that intersects with correct trace t2 = [1, 2, 3, 7, 8, 4, 6].”
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];”
Synthesis of interface specifications for Java classes (2005, neutral): “employed by SLAM for abstracting C code using boolean predicates [5].”
Software model checking (2009, neutral): “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.”