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 27 articles , 1 standard article )

Showing results 1 to 20 of 27.
Sorted by year (citations)

1 2 next

  1. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  2. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
  3. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  4. Mund, Jakob; Huuck, Ralf; Fehnker, Ansgar; Artho, Cyrille: The quest for precision: a layered approach for data race detection in static analysis (2013)
  5. Basler, Gérard; Donaldson, Alastair; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas: SatAbs: a bit-precise verifier for C programs (competition contribution) (2012) ioport
  6. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco: Software model checking with explicit scheduler and symbolic threads (2012)
  7. Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina: A model checking-based approach for security policy verification of mobile systems (2011)
  8. Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp: Automatic analysis of DMA races using model checking and $k$-induction (2011)
  9. Edelkamp, Stefan; Kellershoff, Mark; Sulewski, Damian: Program model checking via action planning (2011) ioport
  10. Seghir, Mohamed Nassim: A lightweight approach for loop summarization (2011)
  11. Artho, Cyrille; Hagiya, Masami; Leungwattanakit, Watcharin; Tanabe, Yoshinori; Yamamoto, Mitsuharu: Model checking of concurrent algorithms: from Java to C (2010)
  12. Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel: Context-aware counter abstraction (2010)
  13. Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: CPBPV: a constraint-programming framework for bounded program verification (2010)
  14. Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Counterexample guided path reduction for static program analysis (2010)
  15. Kroening, Daniel; Weissenbacher, Georg: Verification and falsification of programs with loops using predicate abstraction (2010)
  16. Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel: Symbolic counter abstraction for concurrent software (2009)
  17. Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Incremental false path elimination for static software analysis (2009)
  18. Kattenbelt, Mark; Huth, Michael: Verification and refutation of probabilistic specifications via games (2009)
  19. Schlich, Bastian; Kowalewski, Stefan: Model checking C source code for embedded systems (2009) ioport
  20. Armando, Alessandro; Benerecetti, Massimo; Mantovani, Jacopo: Abstraction refinement of linear programs with arrays (2007)

1 2 next