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

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

1 2 next

  1. Aissat, Romain; Voisin, Frédéric; Wolff, Burkhart: Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths (2016)
  2. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  3. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
  4. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  5. Mund, Jakob; Huuck, Ralf; Fehnker, Ansgar; Artho, Cyrille: The quest for precision: a layered approach for data race detection in static analysis (2013)
  6. 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
  7. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco: Software model checking with explicit scheduler and symbolic threads (2012)
  8. Ermis, Evren; Hoenicke, Jochen; Podelski, Andreas: Splitting via interpolants (2012)
  9. Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina: A model checking-based approach for security policy verification of mobile systems (2011)
  10. Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp: Automatic analysis of DMA races using model checking and $k$-induction (2011)
  11. Edelkamp, Stefan; Kellershoff, Mark; Sulewski, Damian: Program model checking via action planning (2011) ioport
  12. Seghir, Mohamed Nassim: A lightweight approach for loop summarization (2011)
  13. Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel: Loop summarization and termination analysis (2011)
  14. Artho, Cyrille; Hagiya, Masami; Leungwattanakit, Watcharin; Tanabe, Yoshinori; Yamamoto, Mitsuharu: Model checking of concurrent algorithms: from Java to C (2010)
  15. Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel: Context-aware counter abstraction (2010)
  16. Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: CPBPV: a constraint-programming framework for bounded program verification (2010)
  17. Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Counterexample guided path reduction for static program analysis (2010)
  18. Kroening, Daniel; Weissenbacher, Georg: Verification and falsification of programs with loops using predicate abstraction (2010)
  19. Baltazar, Pedro; Mateus, Paulo: Temporalization of probabilistic propositional logic (2009)
  20. Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel: Symbolic counter abstraction for concurrent software (2009)

1 2 next