SatAbs

SATABS: SAT-based predicate abstraction for ANSI-C. This paper presents a model checking tool, SatAbs, that implements a predicate abstraction refinement loop. Existing software verification tools such as Slam, Blast, or Magic use decision procedures for abstraction and simulation that are limited to integers. SatAbs overcomes these limitations by using a SAT-solver. This allows the model checker to handle the semantics of the ANSI-C standard accurately. This includes a sound treatment of bit-vector overflow, and of the ANSI-C pointer arithmetic constructs.


References in zbMATH (referenced in 37 articles , 1 standard article )

Showing results 21 to 37 of 37.
Sorted by year (citations)
  1. Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel: Context-aware counter abstraction (2010)
  2. Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: CPBPV: a constraint-programming framework for bounded program verification (2010)
  3. Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Counterexample guided path reduction for static program analysis (2010)
  4. Kroening, Daniel; Weissenbacher, Georg: Verification and falsification of programs with loops using predicate abstraction (2010)
  5. Baltazar, Pedro; Mateus, Paulo: Temporalization of probabilistic propositional logic (2009)
  6. Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel: Symbolic counter abstraction for concurrent software (2009)
  7. Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Incremental false path elimination for static software analysis (2009)
  8. Kattenbelt, Mark; Huth, Michael: Verification and refutation of probabilistic specifications via games (2009)
  9. Schlich, Bastian; Kowalewski, Stefan: Model checking C source code for embedded systems (2009) ioport
  10. Armando, Alessandro; Benerecetti, Massimo; Mantovani, Jacopo: Abstraction refinement of linear programs with arrays (2007)
  11. Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak: The software model checker blast (2007) ioport
  12. Clarke, Edmund; Jain, Himanshu; Kroening, Daniel: Verification of SpecC using predicate abstraction (2007)
  13. Cook, Byron; Kroening, Daniel; Sharygina, Natasha: Verification of Boolean programs with unbounded thread creation (2007)
  14. Collavizza, Hélène; Rueher, Michel: Exploration of the capabilities of constraint programming for software verification (2006)
  15. Kroening, Daniel; Sharygina, Natasha: Approximating predicate images for bit-vector logic (2006)
  16. Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen: SATABS: SAT-based predicate abstraction for ANSI-C (2005)
  17. Cook, Byron; Kroening, Daniel; Sharygina, Natasha: Cogent: Accurate theorem proving for program verification (2005)