SatAbs swMATH ID: 12804 Software Authors: Clarke, E., Kroning, D., Sharygina, N., Yorav, K. Description: 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. Homepage: http://link.springer.com/chapter/10.1007/978-3-540-31980-1_40 Related Software: BLAST; SLAM; CPAchecker; SPIN; Bebop; CBMC; Zing; UFO; Wolverine; z3; Cogent; KLEE; Orion; DDVerify; SIMPLIFY; Java PathFinder; VCC; CEGAR; ASTREE; FOCI Cited in: 35 Documents Standard Articles 1 Publication describing the Software Year SatAbs: a bit-precise verifier for C programs (competition contribution) Basler, Gérard; Donaldson, Alastair; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas 2012 all top 5 Cited by 71 Authors 12 Kröning, Daniel 7 Sharygina, Natasha 2 Basler, Gérard 2 Clarke, Edmund Melson jun. 2 Collavizza, Hélène 2 Cook, Byron 2 Fehnker, Ansgar 2 Huuck, Ralf 2 Mazzucchi, Michele 2 Podelski, Andreas 2 Rueher, Michel 2 Seefried, Sean 2 Tsitovich, Aliaksei 2 Wahl, Thomas 2 Wintersteiger, Christoph M. 1 Aissat, Romain 1 Armando, Alessandro 1 Artho, Cyrille 1 Baltazar, Pedro 1 Baranowski, Marek 1 Barone-Adesi, Katerina 1 Benerecetti, Massimo 1 Beyer, Dirk 1 Biere, Armin 1 Braghin, Chiara 1 Cimatti, Alessandro 1 Dams, Dennis René 1 Daniel, Jakub 1 Donaldson, Alastair F. 1 Ermis, Evren 1 Garzella, Jack J. 1 Grumberg, Orna 1 Gulwani, Sumit 1 Gupta, Ashutosh 1 Hagiya, Masami 1 Hajdu, Ákos 1 He, Shaobo 1 Henzinger, Thomas A. 1 Hoenicke, Jochen 1 Huth, Michael R. A. 1 Jain, Himanshu 1 Jhala, Ranjit 1 Kattenbelt, Mark 1 Křena, Bohuslav 1 Leungwattanakit, Watcharin 1 Mantovani, Jacopo 1 Mateus, Paulo C. 1 McMillan, Kenneth L. 1 Micskei, Zoltán 1 Narasamdya, Iman 1 Parízek, Pavel 1 Pommellet, Adrien 1 Radhakrishna, Arjun 1 Rakamarić, Zvonimir 1 Roveri, Marco 1 Rümmer, Philipp 1 Rybalchenko, Andrey 1 Samanta, Roopsha 1 Schmidt, David A. 1 Seghir, Mohamed Nassim 1 Tanabe, Yoshinori 1 Tarrach, Thorsten 1 Tonetta, Stefano 1 Touili, Tayssir 1 Van Hentenryck, Pascal 1 Voisin, Frédéric 1 Vojnar, Tomáš 1 Weissenbacher, Georg 1 Wolff, Burkhart 1 Yamamoto, Mitsuharu 1 Yorav, Karen all top 5 Cited in 7 Serials 4 Formal Methods in System Design 2 Formal Aspects of Computing 1 International Journal of General Systems 1 Theoretical Computer Science 1 Journal of Automated Reasoning 1 Constraints 1 Logical Methods in Computer Science Cited in 3 Fields 34 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year