Automatically validating temporal safety properties of interfaces

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

695 citations recorded by the source corpus.

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

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

KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs (2008, unknown): “Similar to symbolic execution systems, model checkers have been used to ﬁnd bugs in both the design and the implementation of software [10,12, 19,25, 29, 30].”
The SLAM Toolkit (2001, methodology): “Given a safety property to check on a C program P , the SLAM process [4] iteratively re(cid:12)nes a boolean program abstraction of P using three tools: { C2bp , a predicate abstraction tool that abstracts P into a boolean program BP ( P; E ) with respect to a set of predicates E over P [1,2]; {…”
A genetic programming approach to automated software repair (2009, background): “Many techniques are available for identifying bugs in programs, both statically (e.g., [7, 16]) and dynamically (e.g., [14, 17, 20]).”
A few billion lines of code later (2010, background): “A glance through the literature reveals many ways to go about static bug finding.(1,2,4,7,8,11) For us, the central religion was results: If it worked, it was good, and if not, not.”
The verifying compiler: A grand challenge for computing research (2003, background): “Program analysis tools are now available which use a variety of techniques to discover relevant invariants and abstractions [37-39].”
EXE: automatically generating inputs of death (2006, methodology): “7.2 Software Model Checking Model checkershavebeenused to .ndbugsinboth thedesignand theimplementation of software[Holzmann1997,2001;Brat et al.2000;Corbett et al. 2000; Ball and Rajamani 2001; Godefroid 1997; Yang et al. 2004].”
Effective typestate verification in the presence of aliasing (2006, background): “[Dwyer and Clarke 1994; Naumovich et al. 1999; Corbett et al. 2000; DeLine and Fähndrich 2001; Ball and Rajamani 2001; Foster et al. 2002; Flanagan et al. 2002; Ashcraft and Engler 2002; Ramalingam et al. 2002; Das et al. 2002; Field et al. 2003]).”
Mining specifications (2002, methodology): “A veri.cation tool that uses the speci.cation to examine all program paths (such as Bebop [2] or xgcc [10]) could then .nd the rare bug.”
Region-based memory management in cyclone (2002, background): “Many systems, including but certainly not limited to LCLint [10, 9], SLAM [3], Safe-C [2], and CCured [25], aim to make C code safe.”
Using formal specifications to support testing (2009, methodology): “More recent approaches, such as the SLAM and BLAST tools, automatically and incrementally construct models from source code by discovering and tracking those predicates over program variables that are relevant to verifying a temporal property at hand.”
Thorough static analysis of device drivers (2006, background): “This harness leads to fewer false errors being reported but results in increased analysis times.”
Static Analysis of Executables to Detect Malicious Patterns (2003, methodology): “b original ✓ ✓ ✓ ✓ obfuscated ✕([1,2]) ✕([1,2]) ✕([1,2]) ✓”
Lazy abstraction (2002, background): “00 One traditional ow for model checking a piece of code proceeds through the following loop [5, 10, 28]: Step 1 (\abstraction") A nite set of predicates is chosen, and an abstractmodel of the given program is built automatically as a nite or push-down automaton whose states represent truth assignme”
Modular verification of software components in C (2003, methodology): “The MAGIC tool follows the well-known abstract - verify - refine paradigm [13, 16, 21, 27]:”