The SLAM Toolkit

By Thomas Ball, Sriram K. Rajamani. International Conference on Computer Aided Verification, 2001

346 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Software

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

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 Software

Citations in the corpus

Dynamic partial-order reduction for model checking software (2005, background): “This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to identify backtracking points where alternative paths in the state space need to be explored.”
Introduction to Embedded Systems - A Cyber-Physical Systems Approach (2013, methodology): “Two examples of abstraction-based software model checking systems are SLAM developed at Microsoft Research (Ball and Rajamani, 2001) and BLAST developed at UC Berkeley (Henzinger et al., 2003b; Beyer et al., 2007). Both methods combine CEGAR with a particular form of abstraction called predicate abs”
WYSINWYX: What you see is not what you eXecute (2010, methodology): “Several approaches to improve the reliability of device drivers have been previously proposed [Ball et al. 2006; Ball and Rajamani 2001; Chou et al. 2001; Swift et al. 2005].”
Global Software Engineering: The Future of Socio-technical Coordination (2007, methodology): “While not usually considered in the context of requirements or GSD, this sort of analysis has in fact been effective in conveying a very complex API to a number of vendors in different organizations.”
Abstract Regular Model Checking (2004, methodology): “, in tools for software model checking like Slam [6], Magic [13], or Blast [19].”
DieHard: probabilistic memory safety for unsafe languages (2006, methodology): “This heap semantics is the same as that assumed by the SLAM toolkit [4] and the BLAST software model checker [19].”
DART: directed automated random testing (2005, methodology): “We now discuss how to implement the algorithms presented in the previous section for testing programs written in the C programming language.”