CBMC resources

Papers

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. Daniel Kroening, Edmund Clarke, and Karen Yorav. In Proceedings of Design Automation Conference (DAC), pages 368-371, 2003.
- This is the original paper on CBMC that was later expanded into the following CMU technical report, which includes a good description of CBMC's internal architecture:
- Behavioral Consistency of C and Verilog Programs. Edmund Clarke, Daniel Kroening, Karen Yorav. CMU-CS-03-126, May 2003.
A number of further applications of CBMC can be found online.

Model checking boot code from AWS data centers. Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle. Formal Methods in System Design, volume 57, number 1, pages 34-52, July 2021.
- This paper originally appeared in the following paper at CAV 2018:
- Model Checking Boot Code from AWS Data Centers. Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle: In Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018), pages 267-486, July 2018.
Code-level model checking in the software development workflow at Amazon Web Services. Nathan Chong, Byron Cook, Jonathan Eidelman, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle. Journal of Software: Practice and Experience --- Special Issue: Introduction to the Special Issue on Software Engineering in Practice, volume 51, issue 4, pages 772-797, April 2021.
- This paper originally appears in the following paper at ICSE 2020:
- Code-Level Model Checking in the Software Development Workflow. Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP 2020), pages 11–20, June 2020.