# CBMC resources

* [CBMC home page](https://www.cprover.org/cbmc/)
* [CBMC github repository](https://github.com/diffblue/cbmc)
* [Papers](#papers)
* [Blog posts](#blog-posts)
* [Talks](#talks)

## Papers

### CBMC technology

* [Behavioral Consistency of C and Verilog Programs Using Bounded Model
  Checking](http://www.kroening.com/papers/dac2003.pdf).
  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](
    http://reports-archive.adm.cs.cmu.edu/anon/2003/CMU-CS-03-126.pdf).
    Edmund Clarke, Daniel Kroening, Karen Yorav.
    CMU-CS-03-126, May 2003.
* A number of further [applications of
  CBMC](https://www.cprover.org/cbmc/applications/) can be found online.

### CBMC applications

* [Model checking boot code from AWS data centers](
  https://link.springer.com/article/10.1007/s10703-020-00344-2).
  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](
    https://link.springer.com/chapter/10.1007/978-3-319-96142-2_28).
    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](
  https://onlinelibrary.wiley.com/doi/epdf/10.1002/spe.2949).
  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](
    https://dl.acm.org/doi/pdf/10.1145/3377813.3381347).
    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

* [Daniel Schwartz-Narbonne shares how automated reasoning is helping
  achieve the provable security of AWS boot code](
  https://aws.amazon.com/blogs/security/automated-reasoning-provable-security-of-boot-code-tlarg/)
  in the [AWS Security Blog](https://aws.amazon.com/blogs/security/).
  Supriya Anand. October 2, 2018.

* [Ensuring the Memory Safety of FreeRTOS Part 1](https://www.freertos.org/2020/02/ensuring-the-memory-safety-of-freertos-part-1.html) and
  [Part 2](https://www.freertos.org/2020/05/ensuring-the-memory-safety-of-freertos-part-2.html) in the
  [FreeRTOS Blog](https://www.freertos.org/blog.html).
   Nathan Chong, February and May 2020.

## Talks

* [Code-level model checking in the software development workflow](
  https://www.youtube.com/watch?v=-EuIrAP9_tU), Daniel Schwartz-Narbonne,
  ICSE 2020 conference talk.