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 86 articles )

Showing results 41 to 60 of 86.
Sorted by year (citations)
  1. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  2. Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg: Under-approximating loops in C programs for fast counterexample detection (2015)
  3. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  4. Zakharov, I. S.; Mutilin, V. S.; Khoroshilov, A. V.: Pattern-based environment modeling for static verification of Linux kernel modules (2015) ioport
  5. Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rezine, Othmane; Stenman, Jari: Budget-bounded model-checking pushdown systems (2014)
  6. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  7. Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel: Deciding floating-point logic with abstract conflict driven clause learning (2014)
  8. Groce, Alex; Havelund, Klaus; Holzmann, Gerard; Joshi, Rajeev; Xu, Ru-Gang: Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (2014)
  9. Kroening, Daniel; Tautschnig, Michael: CBMC - C bounded model checker. (Competition contribution) (2014) ioport
  10. Chaki, Sagar; Gurfinkel, Arie; Kong, Soonho; Strichman, Ofer: Compositional sequentialization of periodic programs (2013)
  11. Chattopadhyay, Sudipta; Roychoudhury, Abhik: Scalable and precise refinement of cache timing analysis via path-sensitive verification (2013)
  12. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  13. Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
  14. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2012)
  15. Grumberg, Orna; Meller, Yael; Yorav, Karen: Applying software model checking techniques for behavioral UML models (2012)
  16. Janičić, Predrag: URSA: a system for uniform reduction to SAT (2012)
  17. Jobstmann, Barbara; Staber, Stefan; Griesmayer, Andreas; Bloem, Roderick: Finding and fixing faults (2012)
  18. Kim, Moonzoo; Kim, Yunho; Choi, Yunja: Concolic testing of the multi-sector Read operation for flash storage platform software (2012) ioport
  19. Mandrykin, M. U.; Mutilin, V. S.; Novikov, E. M.; Khoroshilov, A. V.; Shved, P. E.: Using Linux device drivers for static verification tools benchmarking (2012) ioport
  20. Mühlberg, Jan Tobias; Lüttgen, Gerald: Verifying compiled file system code (2012) ioport