diff --git a/docs/README.md b/docs/README.md index 1c7870b..7bf0186 100644 --- a/docs/README.md +++ b/docs/README.md @@ -65,8 +65,9 @@ appreciated! -## 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