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

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

1 2 3 next

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

1 2 3 next