CBMC

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

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

1 2 3 4 next

  1. Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
  2. Guthmuller, Marion; Corona, Gabriel; Quinson, Martin: System-level state equality detection for the formal dynamic verification of legacy distributed applications (2018)
  3. Abal, Iago; Brabrand, Claus; Wąsowski, Andrzej: Effective bug finding in C programs with shape and effect abstractions (2017)
  4. Büscher, Niklas; Franz, Martin; Holzer, Andreas; Veith, Helmut; Katzenbeisser, Stefan: On compiling Boolean circuits optimized for secure multi-party computation (2017)
  5. Č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)
  6. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  7. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  8. Demyanova, Yulia; Pani, Thomas; Veith, Helmut; Zuleger, Florian: Empirical software metrics for benchmarking of verification tools (2017)
  9. Hutter, Frank; Lindauer, Marius; Balint, Adrian; Bayless, Sam; Hoos, Holger; Leyton-Brown, Kevin: The configurable SAT solver challenge (CSSC) (2017)
  10. Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom: Incremental bounded model checking for embedded software (2017)
  11. Wang, Wei; Barrett, Clark; Wies, Thomas: Partitioned memory models for program analysis (2017)
  12. Yeolekar, Anand; Madhukar, Kumar; Bhutada, Dipali; Venkatesh, R.: Sequentialization using timestamps (2017)
  13. Bagnara, Roberto; Carlier, Matthieu; Gori, Roberta; Gotlieb, Arnaud: Exploiting binary floating-point representations for constraint propagation (2016)
  14. KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: SATenstein: automatically building local search SAT solvers from components (2016)
  15. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
  16. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
  17. Travkin, Oleg; Wehrheim, Heike: Verification of concurrent programs on weak memory models (2016)
  18. Balint, Adrian; Belov, Anton; Järvisalo, Matti; Sinz, Carsten: Overview and analysis of the SAT challenge 2012 solver competition (2015) ioport
  19. Chaki, Sagar; Gurfinkel, Arie; Strichman, Ofer: Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation) (2015)
  20. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)

1 2 3 4 next