Skip to content

Commit 894567d

Browse files
authored
Update README.md - add link to Fulminate paper (#105)
1 parent 9f6c7a6 commit 894567d

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

docs/README.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -65,8 +65,9 @@ appreciated!
6565

6666
</div>
6767

68-
## Origins
69-
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.
68+
## Origins and papers
69+
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.
70+
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.
7071
To accurately handle the complex semantics of C, CN builds on the [Cerberus semantics for C](https://github.com/rems-project/cerberus/).
7172
Some of the examples in this tutorial are adapted from Arthur Charguéraud’s excellent
7273
[Separation Logic Foundations](https://softwarefoundations.cis.upenn.edu) textbook, and one of the case studies is based on an

0 commit comments

Comments
 (0)