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.
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Travkin, Oleg; Wehrheim, Heike: Verification of concurrent programs on weak memory models (2016)
- Grumberg, Orna; Meller, Yael; Yorav, Karen: Applying software model checking techniques for behavioral UML models (2012)
- Brillout, Angelo; He, Nannan; Mazzucchi, Michele; Kroening, Daniel; Purandare, Mitra; Rümmer, Philipp; Weissenbacher, Georg: Mutation-based test case generation for Simulink models (2010)
- Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: CPBPV: a constraint-programming framework for bounded program verification (2010)
- Angeletti, Damiano; Giunchiglia, Enrico; Narizzano, Massimo; Puddu, Alessandra; Sabina, Salvatore: Automatic test generation for coverage analysis using CBMC (2009)
- Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: Comparison between CPBPV, ESC/Java, CBMC, blast, EUREKA and why for bounded program verification (2008)