SATABS: SAT-Based Predicate Abstraction for ANSI-C

By Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav. International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2005

307 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.

CPAchecker: A Tool for Configurable Software Verification (2009, methodology): “The advantage of the new tool over tools that implement a separated abstract-check-refine loop, like Slam [1] and SATabs [ 8 ], is that the on-the-fly approach allows the design of more flexible, and more efficient, algorithms (like ABE [5]).”
The software model checker Blast (2007, methodology): “Implementations of CEGAR include Slam, Blast, Magic, Moped, SatAbs, and F- Soft [4,17,23,33,54].”
Lazy Abstraction with Interpolants (2006, methodology): “This reduction was done using a modified version of the SATABS infrastructure [4].”