×

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, ex­cep­tions and user-specified as­ser­tions. 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 re­sul­ting 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; SPIN; BLAST; z3; CPAchecker; SLAM; Chaff; GitHub; CIL; ASTREE; DART; NuSMV; SatAbs; KLEE; Java PathFinder; SMT-LIB; CUTE; SATzilla; veriSoft; LLVM
Referenced in: 74 Publications
all top 5

Referenced by 233 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 133 more Authors
all top 5

Referenced in 19 Serials

15 Formal Methods in System Design
4 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

Referenced in 8 Fields

72 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)

Referencing Publications by Year