From 61ee668bb64e67132e9f4d2d6a9eb6ddffdcaf6d Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Sat, 23 Nov 2024 07:58:44 +0000 Subject: [PATCH] Update README.md - add link to Fulminate paper --- docs/README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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