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 1 to 20 of 86.
Sorted by year (citations)

1 2 3 4 5 next

  1. Bhattacharyya, Arnab; Gupta, Ashutosh; Kuppusamy, Lakshmanan; Mani, Somya; Shukla, Ankit; Srivas, Mandayam; Thattai, Mukund: A formal methods approach to predicting new features of the eukaryotic vesicle traffic system (2021)
  2. Cook, Byron; Khazem, Kareem; Kroening, Daniel; Tasiran, Serdar; Tautschnig, Michael; Tuttle, Mark R.: Model checking boot code from AWS data centers (2021)
  3. Hajdu, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei: Inductive benchmarks for automated reasoning (2021)
  4. Heldmann, Tim; Schneider, Thomas; Tkachenko, Oleksandr; Weinert, Christian; Yalame, Hossein: LLVM-based circuit compilation for practical secure computation (2021)
  5. Manthey, Norbert: The \textscMergeSatsolver (2021)
  6. Ponzio, Pablo; Godio, Ariel; Rosner, Nicolás; Arroyo, Marcelo; Aguirre, Nazareno; Frias, Marcelo F.: Efficient bounded model checking of heap-manipulating programs using tight field bounds (2021)
  7. Abate, Alessandro; Bessa, Iury; Cordeiro, Lucas; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth: Automated formal synthesis of provably safe digital controllers for continuous plants (2020)
  8. Semenov, Alexander; Otpuschennikov, Ilya; Gribanova, Irina; Zaikin, Oleg; Kochemazov, Stepan: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems (2020)
  9. Tellez, Gadi; Brotherston, James: Automatically verifying temporal properties of pointer programs with cyclic proof (2020)
  10. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Yao, Chenguang: Translating Xd-C programs to MSVL programs (2020)
  11. Bouajjani, Ahmed; Enea, Constantin; Lahiri, Shuvendu K.: Abstract semantic diffing of evolving concurrent programs (2019)
  12. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
  13. Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
  14. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  15. Biere, Armin; Kröning, Daniel: SAT-based model checking (2018)
  16. Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W.: VST-Floyd: a separation logic tool to verify correctness of C programs (2018)
  17. Chaves, Lennon; Bessa, Iury; Cordeiro, Lucas; Kroening, Daniel: DSValidator: an automated counterexample reproducibility tool for digital systems (2018)
  18. Duck, Gregory J.; Jaffar, Joxan; Yap, Roland H. C.: Shape neutral analysis of graph-based data-structures (2018)
  19. Guthmuller, Marion; Corona, Gabriel; Quinson, Martin: System-level state equality detection for the formal dynamic verification of legacy distributed applications (2018)
  20. Kurshan, Robert P.: Transfer of model checking to industrial practice (2018)

1 2 3 4 5 next