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 41 to 60 of 77.
Sorted by year (citations)
  1. Chaki, Sagar; Gurfinkel, Arie; Kong, Soonho; Strichman, Ofer: Compositional sequentialization of periodic programs (2013)
  2. Chattopadhyay, Sudipta; Roychoudhury, Abhik: Scalable and precise refinement of cache timing analysis via path-sensitive verification (2013)
  3. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  4. Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
  5. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2012)
  6. Grumberg, Orna; Meller, Yael; Yorav, Karen: Applying software model checking techniques for behavioral UML models (2012)
  7. Janičić, Predrag: URSA: a system for uniform reduction to SAT (2012)
  8. Jobstmann, Barbara; Staber, Stefan; Griesmayer, Andreas; Bloem, Roderick: Finding and fixing faults (2012)
  9. Kim, Moonzoo; Kim, Yunho; Choi, Yunja: Concolic testing of the multi-sector Read operation for flash storage platform software (2012) ioport
  10. 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
  11. Mühlberg, Jan Tobias; Lüttgen, Gerald: Verifying compiled file system code (2012) ioport
  12. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2011)
  13. Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp: Automatic analysis of DMA races using model checking and (k)-induction (2011)
  14. Wang, Chao; Kundu, Sudipta; Limaye, Rhishikesh; Ganai, Malay; Gupta, Aarti: Symbolic predictive analysis for concurrent programs (2011)
  15. Brillout, Angelo; He, Nannan; Mazzucchi, Michele; Kroening, Daniel; Purandare, Mitra; Rümmer, Philipp; Weissenbacher, Georg: Mutation-based test case generation for Simulink models (2010)
  16. Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: CPBPV: a constraint-programming framework for bounded program verification (2010)
  17. Hoenicke, Jochen; Leino, K. Rustan M.; Podelski, Andreas; Schäf, Martin; Wies, Thomas: Doomed program points (2010)
  18. Kolchin, A. V.: An automatic method for the dynamic construction of abstractions of states of a formal model (2010)
  19. Malacaria, Pasquale; Heusser, Jonathan: Information theory and security: Quantitative information flow (2010)
  20. Angeletti, Damiano; Giunchiglia, Enrico; Narizzano, Massimo; Puddu, Alessandra; Sabina, Salvatore: Automatic test generation for coverage analysis using CBMC (2009) ioport