The software model checker Blast

By Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar. International Journal on Software Tools for Technology Transfer (STTT), 2007

546 citations recorded by the source corpus.

How researchers see this paper

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

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).”
Software model checking (2009, unknown): “For example, Blast combines predicate abstraction with arbitrary other abstractions speciﬁed via a lattice [Fischer et al. 2005; Beyer et al. 2007].”
CPAchecker: A Tool for Configurable Software Verification (2009, methodology): “For example, the tool can run a predicate analysis using single-block encoding (SBE), like Blast [ 3 ] and Slam [1], but also using large-block encoding (LBE) [2] or even adjustable-block encoding (ABE) [5].”