The SLAM project: debugging system software via static analysis

By Thomas Ball, Sriram K. Rajamani. 2002

995 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Information Systems, Software

How researchers see this paper

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

In Computational Theory and Mathematics

In Information Systems

In Software

Citations in the corpus

Formal Security Analysis of Neural Networks using Symbolic Intervals (2018, methodology): “As we also know 2x+ 3y > 0 and x+ y > 0 for the given input range x ∈ [4,6] and y ∈ [1,5], we can safely propagate this symbolic interval through the ReLU activation function.”
Learning a strategy for adapting a program analysis via bayesian optimisation (2015, methodology): “Such analyses commonly adopt counter-example-guided abstraction refinement, and selects a program abstraction based on the feedback from a failed analysis run [1, 4–6, 8, 9, 31, 32].”
Z3: An Efficient SMT Solver (2008, methodology): “It is being integrated with other projects, including SLAM/SDV [1].”
Finding bugs is easy (2004, methodology): “Often, these techniques rely on formal methods and sophisticated program analysis.”
Test input generation with java PathFinder (2004, methodology): “There has been a lot of recent interest in applying model checking to software [7,8,15,17,22,27,43].”
CPAchecker: A Tool for Configurable Software Verification (2009, methodology): “ed to eliminate, most prominently, that the architecture and the design are not ﬂexible enough to implement a pure CPA-based analysis. As in the Blast project already, many ideas were taken from Slam [2]. The source code, executables, and all benchmark programs for CPAchecker are available online at”
The software model checker Blast (2007, methodology): “A key paradigm behind some of the new software verification tools is the principle of counterexample-guided abstraction refinement (CEGAR) [1,3,4,21,49,61,78].”
From symptom to cause: localizing errors in counterexample traces (2003, methodology): “In recent years, model checking has gained wider use in checking properties of software [13, 7, 3].”
MOPS: an infrastructure for examining security properties of software (2002, methodology): “SLAM [2, 3] is a pioneer project that uses software model checking to verify temporal safety properties in programs.”
Lazy Abstraction with Interpolants (2006, methodology): “This is implemented using the lazy paradigm in the Blast model checker [7], and in a number of software model checkers [2,4,3] using a counterexamplebased refinement loop.”
A static analyzer for large safety-critical software (2003, background): “alyzers. 9.2 Dataﬂow Analysis and Software Abstract Model Checking Dataﬂow analyzers (such as ESP [14]) as well as abstraction based software model checkers (such as a.o. Blast [21], CMC [31] and Slam[4]) have made large inroads in tackling programs of comparable size and complexity. Their impressiv”
Liquid types (2008, methodology): “Predicate abstraction has proven effective for path-sensitive verification of control-dominated properties of first-order imperative programs [3, 16, 11, 4, 29, 17].”
Secure Information Flow as a Safety Problem (2005, methodology): “Both SLAM and BLAST combine theorem proving and model checking in an iteratively refining manner to achieve robust safety analysis that can scale to programs of non-trivial size written in feature-rich programming languages like C.”
Automatic mining of source code repositories to improve bug finding techniques (2005, background): “Static analysis of source code to locate bugs is a wellresearched area [3], [16].”
Debugging in the (very) large: ten years of implementation and experience (2009, methodology): “We continue to apply static analysis and model-checking tools to find errors early in the development process [2, 3].”