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

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

1 2 next

  1. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  2. Biere, Armin; Kröning, Daniel: SAT-based model checking (2018)
  3. Dams, Dennis; Grumberg, Orna: Abstraction and abstraction refinement (2018)
  4. Jhala, Ranjit; Podelski, Andreas; Rybalchenko, Andrey: Predicate abstraction for program verification (2018)
  5. McMillan, Kenneth L.: Interpolation and model checking (2018)
  6. Aissat, Romain; Voisin, Frédéric; Wolff, Burkhart: Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths (2016)
  7. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  8. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
  9. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  10. Mund, Jakob; Huuck, Ralf; Fehnker, Ansgar; Artho, Cyrille: The quest for precision: a layered approach for data race detection in static analysis (2013)
  11. 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
  12. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco: Software model checking with explicit scheduler and symbolic threads (2012)
  13. Ermis, Evren; Hoenicke, Jochen; Podelski, Andreas: Splitting via interpolants (2012)
  14. Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina: A model checking-based approach for security policy verification of mobile systems (2011)
  15. Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp: Automatic analysis of DMA races using model checking and $k$-induction (2011)
  16. Edelkamp, Stefan; Kellershoff, Mark; Sulewski, Damian: Program model checking via action planning (2011) ioport
  17. Seghir, Mohamed Nassim: A lightweight approach for loop summarization (2011)
  18. Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel: Loop summarization and termination analysis (2011)
  19. Artho, Cyrille; Hagiya, Masami; Leungwattanakit, Watcharin; Tanabe, Yoshinori; Yamamoto, Mitsuharu: Model checking of concurrent algorithms: from Java to C (2010)
  20. Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel: Context-aware counter abstraction (2010)

1 2 next