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

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

1 2 next

  1. Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir: Leveraging compiler intermediate representation for multi- and cross-language verification (2020)
  2. Hajdu, Ákos; Micskei, Zoltán: Efficient strategies for CEGAR-based model checking (2020)
  3. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  4. Biere, Armin; Kröning, Daniel: SAT-based model checking (2018)
  5. Dams, Dennis; Grumberg, Orna: Abstraction and abstraction refinement (2018)
  6. Jhala, Ranjit; Podelski, Andreas; Rybalchenko, Andrey: Predicate abstraction for program verification (2018)
  7. McMillan, Kenneth L.: Interpolation and model checking (2018)
  8. Aissat, Romain; Voisin, Frédéric; Wolff, Burkhart: Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths (2016)
  9. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  10. Daniel, Jakub; Parízek, Pavel: Predicate abstraction in program verification: survey and current trends (2014)
  11. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
  12. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  13. Mund, Jakob; Huuck, Ralf; Fehnker, Ansgar; Artho, Cyrille: The quest for precision: a layered approach for data race detection in static analysis (2013) ioport
  14. 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
  15. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco: Software model checking with explicit scheduler and symbolic threads (2012)
  16. Ermis, Evren; Hoenicke, Jochen; Podelski, Andreas: Splitting via interpolants (2012)
  17. Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina: A model checking-based approach for security policy verification of mobile systems (2011)
  18. Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp: Automatic analysis of DMA races using model checking and (k)-induction (2011)
  19. Edelkamp, Stefan; Kellershoff, Mark; Sulewski, Damian: Program model checking via action planning (2011) ioport
  20. Seghir, Mohamed Nassim: A lightweight approach for loop summarization (2011)

1 2 next