Skip to content

Commit

Permalink
Update README.md - add link to Fulminate paper
Browse files Browse the repository at this point in the history
  • Loading branch information
PeterSewell authored Nov 23, 2024
1 parent 9f6c7a6 commit 61ee668
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions docs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,9 @@ appreciated!

</div>

## Origins
CN was first described in [CN: Verifying Systems C Code with Separation-Logic Refinement Types](https://dl.acm.org/doi/10.1145/3571194) by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami.
## Origins and papers
CN was first described in [CN: Verifying Systems C Code with Separation-Logic Refinement Types](https://dl.acm.org/doi/10.1145/3571194) by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami, in POPL 2023.
The Fulminate system for runtime testing of CN specifications was first described in [Fulminate: Testing CN Separation-Logic Specifications in C](http://www.cl.cam.ac.uk/users/pes20/cn-testing-popl2025.pdf), by Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte, Neel Krishnaswami, and Peter Sewell, in POPL 2025.
To accurately handle the complex semantics of C, CN builds on the [Cerberus semantics for C](https://github.com/rems-project/cerberus/).
Some of the examples in this tutorial are adapted from Arthur Charguéraud’s excellent
[Separation Logic Foundations](https://softwarefoundations.cis.upenn.edu) textbook, and one of the case studies is based on an
Expand Down

0 comments on commit 61ee668

Please sign in to comment.