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.

References in zbMATH (referenced in 77 articles )

Showing results 61 to 77 of 77.
Sorted by year (citations)
  1. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2009) ioport
  2. Cousot, Patrick; Cousot, Radhia; Feret, Jérôme; Mauborgne, Laurent; Miné, Antoine; Rival, Xavier: Why does Astrée scale up? (2009)
  3. de la Cámara, Pedro; del Mar Gallardo, María; Merino, Pedro; Sanán, David: Checking the reliability of socket based communication software (2009) ioport
  4. Prantl, Adrian; Knoop, Jens; Kirner, Raimund; Kadlec, Albrecht; Schordan, Markus: From trusted annotations to verified knowledge (2009) ioport
  5. Schlich, Bastian; Kowalewski, Stefan: Model checking C source code for embedded systems (2009) ioport
  6. Amjad, Hasan: Data compression for proof replay (2008)
  7. Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: Comparison between CPBPV, ESC/Java, CBMC, blast, EUREKA and why for bounded program verification (2008) ioport
  8. Groce, Alex; Joshi, Rajeev: Exploiting traces in static program analysis: Better model checking through \textttprintfs (2008) ioport
  9. Hermanns, Holger; Palsberg, Jens: Improving the effectiveness of system verification (2008) ioport
  10. Ivančić, Franjo; Yang, Zijiang; Ganai, Malay K.; Gupta, Aarti; Ashar, Pranav: Efficient SAT-based bounded model checking for software verification (2008)
  11. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using abstract transformers (2008)
  12. Shimizu, Hiroaki; Hamaguchi, Kiyoharu; Kashiwabara, Toshinobu: Approximate invariant property checking using term-height reduction for a subset of first-order logic (2008)
  13. Currie, David; Feng, Xiushan; Fujita, Masahiro; Hu, Alan J.; Kwan, Mark; Rajan, Sreeranga: Embedded software verification using symbolic execution and uninterpreted functions (2006)
  14. Groce, Alex; Chaki, Sagar; Kroening, Daniel; Strichman, Ofer: Error explanation with distance metrics (2006) ioport
  15. Moy, Matthieu; Maraninchi, Florence; Maillet-Contoz, Laurent: LusSy: An open tool for the analysis of systems-on-a-chip at the transaction level (2006) ioport
  16. Talpin, Jean-Pierre; Guernic, Paul Le; Shukla, Sandeep Kumar; Gupta, Rajesh: A compositional behavioral modeling framework for embedded system design and conformance checking (2005)
  17. Clarke, Edmund; Kroening, Daniel; Lerda, Flavio: A tool for checking ANSI-C programs (2004)