CBMC swMATH ID: 9719 Software Authors: Clarke E, Kroening D, Lerda F Description: CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions. Furthermore, it can check ANSI-C and C++ for consistency with other languages, such as Verilog. The verification is performed by unwinding the loops in the program and passing the resulting equation to a decision procedure. While CBMC is aimed for embedded software, it also supports dynamic memory allocation using malloc and new. For questions about CBMC, contact Daniel Kroening. Homepage: http://www.cprover.org/cbmc/ Related Software: MiniSat; BLAST; SPIN; z3; CPAchecker; SLAM; Chaff; GitHub; SMT-LIB; CIL; ASTREE; DART; NuSMV; SatAbs; KLEE; Java PathFinder; CUTE; CVC4; SATzilla; SMACK Cited in: 75 Publications all top 5 Cited by 236 Authors 12 Kröning, Daniel 3 Chaki, Sagar 3 Duan, Zhenhua 3 Gurfinkel, Arie 3 Sharygina, Natasha 3 Tian, Cong 3 Zhang, Nan 2 Bardin, Sébastien 2 Bessa, Iury 2 Beyer, Dirk 2 Brain, Martin 2 Brauer, Jörg 2 Clarke, Edmund Melson jun. 2 Cordeiro, Lucas 2 Ganai, Malay K. 2 Gupta, Aarti 2 Gupta, Ashutosh 2 Hoos, Holger H. 2 King, Andy 2 Leyton-Brown, Kevin 2 Podelski, Andreas 2 Rümmer, Philipp 2 Strichman, Ofer 2 Tonetta, Stefano 2 Tsitovich, Aliaksei 2 Veith, Helmut 2 Wang, Meng 2 Weissenbacher, Georg 2 Wies, Thomas 2 Wintersteiger, Christoph M. 2 Zaikin, Oleg Sergeevich 1 Abate, Alessandro 1 Abdulla, Parosh Aziz 1 Ábrahám, Erika 1 Aguirre, Nazareno M. 1 Akhundov, Murad 1 Al-Yahya, Tasniem Nasser 1 Alberti, Francesco 1 Amjad, Hasan 1 Appel, Andrew W. 1 Arroyo, Marcelo 1 Ashar, Pranav 1 Atig, Mohamed Faouzi 1 Bagnara, Roberto 1 Balint, Adrian 1 Barnat, Jiří 1 Barrett, Clark W. 1 Bayless, Sam 1 Beringer, Lennart 1 Bhattacharyya, Arnab 1 Bhutada, Dipali 1 Bienmüller, Tom 1 Biere, Armin 1 Bloem, Roderick 1 Bobot, François 1 Boston, Brett 1 Bouajjani, Ahmed 1 Breese, Samuel 1 Brillout, Angelo 1 Brotherston, James 1 Bruttomesso, Roberto 1 Büscher, Niklas 1 Cao, Qinxiang 1 Carlier, Matthieu 1 Černý, Pavol 1 Chakraborty, Supratik 1 Chattopadhyay, Sudipta 1 Chaves, Lennon 1 Chechik, Marsha 1 Chihani, Zakaria 1 Collavizza, Hélène 1 Cook, Byron 1 Corona, Gabriel 1 Cousot, Patrick 1 Cousot, Radhia 1 Currie, David J. 1 Dangl, Matthias 1 David, Cristina 1 Demyanova, Yulia 1 Dietsch, Daniel 1 Dodds, Joey 1 Dodds, Josiah 1 Dodds, Mike 1 Donaldson, Alastair F. 1 D’silva, Vijay 1 Du, Hongwei 1 Duck, Gregory J. 1 El-bachir Menai, Mohamed 1 Enea, Constantin 1 Farinier, Benjamin 1 Feng, Nick 1 Feng, Xiushan 1 Feret, Jérôme 1 Franz, Martin 1 Fu, Yu-Fu 1 Fujita, Masahiro 1 Ghilardi, Silvio 1 Girol, Guillaume 1 Godio, Ariel 1 Gori, Roberta ...and 136 more Authors all top 5 Cited in 19 Serials 15 Formal Methods in System Design 5 Journal of Automated Reasoning 3 Theoretical Computer Science 3 Logical Methods in Computer Science 2 Acta Informatica 2 Artificial Intelligence 2 International Journal of Parallel Programming 2 Formal Aspects of Computing 2 Journal of Logical and Algebraic Methods in Programming 1 Journal of Computer and System Sciences 1 Journal of Computer Science and Technology 1 Real-Time Systems 1 Cybernetics and Systems Analysis 1 Annals of Mathematics and Artificial Intelligence 1 Constraints 1 INFORMS Journal on Computing 1 Optimization Methods & Software 1 Journal of Combinatorial Optimization 1 Theory and Practice of Logic Programming all top 5 Cited in 8 Fields 73 Computer science (68-XX) 6 Mathematical logic and foundations (03-XX) 4 Information and communication theory, circuits (94-XX) 2 Operations research, mathematical programming (90-XX) 2 Systems theory; control (93-XX) 1 Numerical analysis (65-XX) 1 Fluid mechanics (76-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year