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

Showing results 1 to 20 of 48.
Sorted by year (citations)

1 2 3 next

  1. Černý, Pavol; Clarke, Edmund M.; Henzinger, Thomas A.; Radhakrishna, Arjun; Ryzhyk, Leonid; Samanta, Roopsha; Tarrach, Thorsten: From non-preemptive to preemptive scheduling using synchronization synthesis (2017)
  2. Demyanova, Yulia; Pani, Thomas; Veith, Helmut; Zuleger, Florian: Empirical software metrics for benchmarking of verification tools (2017)
  3. Bagnara, Roberto; Carlier, Matthieu; Gori, Roberta; Gotlieb, Arnaud: Exploiting binary floating-point representations for constraint propagation (2016)
  4. KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: SATenstein: automatically building local search SAT solvers from components (2016)
  5. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
  6. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
  7. Travkin, Oleg; Wehrheim, Heike: Verification of concurrent programs on weak memory models (2016)
  8. Balint, Adrian; Belov, Anton; Järvisalo, Matti; Sinz, Carsten: Overview and analysis of the SAT challenge 2012 solver competition (2015) ioport
  9. Chaki, Sagar; Gurfinkel, Arie; Strichman, Ofer: Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation) (2015)
  10. Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg: Under-approximating loops in C programs for fast counterexample detection (2015)
  11. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  12. Zakharov, I.S.; Mutilin, V.S.; Khoroshilov, A.V.: Pattern-based environment modeling for static verification of Linux kernel modules (2015) ioport
  13. Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rezine, Othmane; Stenman, Jari: Budget-bounded model-checking pushdown systems (2014)
  14. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  15. Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel: Deciding floating-point logic with abstract conflict driven clause learning (2014)
  16. Groce, Alex; Havelund, Klaus; Holzmann, Gerard; Joshi, Rajeev; Xu, Ru-Gang: Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (2014)
  17. Chattopadhyay, Sudipta; Roychoudhury, Abhik: Scalable and precise refinement of cache timing analysis via path-sensitive verification (2013)
  18. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  19. Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
  20. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2012)

1 2 3 next