CBMC resources

Papers

CBMC technology

CBMC applications

  • 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.

Blog posts

Talks