{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:48Z","timestamp":1780994568512,"version":"3.54.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100014013","name":"UKRI","doi-asserted-by":"crossref","award":["EP\/Y035976\/1"],"award-info":[{"award-number":["EP\/Y035976\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Resarch Council","award":["ERC-AdG-2017 789108"],"award-info":[{"award-number":["ERC-AdG-2017 789108"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    Separation logic has become an important tool for formally capturing and reasoning about the ownership patterns of imperative programs, originally for paper proof, and now the foundation for industrial static analyses and multiple proof tools. However, there has been very little work on program\n                    <jats:italic toggle=\"yes\">testing<\/jats:italic>\n                    of separationlogic specifications in concrete execution. At first sight, separation-logic formulas are hard to evaluate in reasonable time, with their implicit quantification over heap splittings, and other explicit existentials.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper we observe that a restricted fragment of separation logic, adopted in the CN proof tool to enable predictable proof automation, also has a natural and readable\n                    <jats:italic toggle=\"yes\">computational<\/jats:italic>\n                    interpretation, that makes it practically usable in runtime testing. We discuss various design issues and develop this as a\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mtext>C<\/mml:mtext>\n                          <mml:mo>+<\/mml:mo>\n                          <mml:mtext>CN<\/mml:mtext>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    source to C source translation, Fulminate. This adds checks \u2013 including ownership checks and ownership transfer \u2013 for C code annotated with CN pre- and post-conditions; we demonstrate this on nontrivial examples, including the allocator from a production hypervisor. We formalise our runtime ownership testing scheme, showing (and proving) how its reified ghost state correctly captures ownership passing, in a semantics for a small C-like language.\n                  <\/jats:p>","DOI":"10.1145\/3704879","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1260-1292","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Fulminate: Testing CN Separation-Logic Specifications in C"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-6360-3972","authenticated-orcid":false,"given":"Rini","family":"Banerjee","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3723-636X","authenticated-orcid":false,"given":"Kayvan","family":"Memarian","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7220-4991","authenticated-orcid":false,"given":"Dhruv","family":"Makwana","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7369-183X","authenticated-orcid":false,"given":"Christopher","family":"Pulte","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2838-5865","authenticated-orcid":false,"given":"Neel","family":"Krishnaswami","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9352-1013","authenticated-orcid":false,"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"2024. Infer. https:\/\/fbinfer.com\/. Accessed 2024-07-08."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676972"},{"key":"e_1_3_2_4_2","volume-title":"Verifiable C. Software Foundations","author":"Appel Andrew W.","year":"2023","unstructured":"Andrew W. Appel, Lennart Beringer, and Qinxiang Cao. 2023. Verifiable C. Software Foundations, Vol. 5. Electronic textbook. https:\/\/softwarefoundations.cis.upenn.edu Version 1.2.2."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"e_1_3_2_6_2","unstructured":"Rini Banerjee Kayvan Memarian Dhruv Makwana Christopher Pulte Neel Krishnaswami and Peter Sewell. 2024. Supplementary material for Fulminate: Testing CN Separation-Logic Specifications in C. Online http:\/\/www.cl.cam.ac.uk\/users\/pes20\/cn-testing-popl2025.pdf accessed 2024-11-23."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38828-6_10"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837621"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45294-X_10"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_2_12_2","volume-title":"Separation Logic Foundations. Software Foundations","author":"Chargu\u00e9raud Arthur","year":"2024","unstructured":"Arthur Chargu\u00e9raud. 2024. Separation Logic Foundations. Software Foundations, Vol. 6. Electronic textbook. https:\/\/softwarefoundations.cis.upenn.edu Version 2.2."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_25"},{"key":"e_1_3_2_14_2","unstructured":"Will Deacon. 2020. Virtualisation for the Masses: Exposing KVM on Android. KVM Forum slides https:\/\/mirrors.edge.kernel.org\/pub\/linux\/kernel\/people\/will\/slides\/kvmforum-2020-edited.pdf. Accessed 2022-07-07."},{"key":"e_1_3_2_15_2","unstructured":"Will Deacon. 2020. Virtualization for the Masses: Exposing KVM on Android. https:\/\/www.youtube.com\/watch?v=wY-u6n75iXc. KVM Forum Talk."},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2480362.2480593"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2017.35"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187678"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Bart Jacobs Jan Smans and Frank Piessens. 2024. The VeriFast Program Verifier: A Tutorial. https:\/\/doi.org\/10.5281\/zenodo.13380705 10.5281\/zenodo.13380705","DOI":"10.5281\/zenodo.13380705"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/1369322"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Nikolai Kosmatov Claude March\u00e9 Yannick Moy and Julien Signoles. 2016. Static versus Dynamic Verification in Why3 Frama-C and SPARK 2014. In Leveraging Applications of Formal Methods Verification and Validation: Foundational Techniques - 7th International Symposium ISoLA 2016 Imperial Corfu Greece October 10-14 2016 Proceedings Part I (Lecture Notes in Computer Science Vol. 9952) Tiziana Margaria and Bernhard Steffen (Eds.). 461\u2013478. https:\/\/doi.org\/10.1007\/978-3-319-47166-2_32 10.1007\/978-3-319-47166-2_32","DOI":"10.1007\/978-3-319-47166-2_32"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/954666.971189"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39656-7_11"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Pablo L\u00f3pez Frank Pfenning Jeff Polakow and Kevin Watkins. 2005. Monadic concurrent linear logic programming. In Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming July 11-13 2005 Lisbon Portugal Pedro Barahona and Amy P. Felty (Eds.). ACM 35\u201346. https:\/\/doi.org\/10.1145\/1069774.1069778 10.1145\/1069774.1069778","DOI":"10.1145\/1069774.1069778"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.230345"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103673"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_38"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1411304.1411311"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.48456\/tr-981"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Kayvan Memarian Victor B. F. Gomes Brooks Davis Stephen Kell Alexander Richardson Robert N. M. Watson and Peter Sewell. 2019. Exploring C Semantics and Pointer Provenance. In Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages. https:\/\/doi.org\/10.1145\/3290380 10.1145\/3290380 Proc. ACM Program. Lang. 3 POPL Article 67. Also available as ISO\/IEC JTC1\/SC22\/WG14 N2311.","DOI":"10.1145\/3290380"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_8"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-810-5-104"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Huu Hai Nguyen Viktor Kuncak and Wei-Ngan Chin. 2008. Runtime Checking for Separation Logic. In Verification Model Checking and Abstract Interpretation 9th International Conference VMCAI 2008 San Francisco USA January 7-9 2008 Proceedings (Lecture Notes in Computer Science Vol. 4905) Francesco Logozzo Doron A. Peled and Lenore D. Zuck (Eds.). Springer 203\u2013217. https:\/\/doi.org\/10.1007\/978-3-540-78163-9_19 10.1007\/978-3-540-78163-9_19","DOI":"10.1007\/978-3-540-78163-9_19"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173723"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/SCAM.2014.19"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41135-4_8"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Christopher Pulte Dhruv C. Makwana Thomas Sewell Kayvan Memarian Peter Sewell and Neel Krishnaswami. 2023. CN: Verifying systems C code with separation-logic refinement types. In Proceedings of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages. https:\/\/doi.org\/10.1145\/3571194 10.1145\/3571194","DOI":"10.1145\/3571194"},{"key":"e_1_3_2_43_2","unstructured":"Christopher Pulte Benjamin C. Pierce Cole Schlesinger and Elizabeth Austell. 2024. CN tutorial. https:\/\/rems-project.github.io\/cn-tutorial\/. [Online; accessed 26-October-2024]."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Michael Sammler Rodolphe Lepigre Robbert Krebbers Kayvan Memarian Derek Dreyer and Deepak Garg. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. In PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation Virtual Event Canada June 20-25 2021 Stephen N. Freund and Eran Yahav (Eds.). ACM 158\u2013174. https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386014"},{"key":"e_1_3_2_48_2","first-page":"309","volume-title":"2012 USENIX Annual Technical Conference, Boston, MA, USA, June 13-15, 2012","author":"Serebryany Konstantin","year":"2012","unstructured":"Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitriy Vyukov. 2012. AddressSanitizer: A Fast Address Sanity Checker. In 2012 USENIX Annual Technical Conference, Boston, MA, USA, June 13-15, 2012, Gernot Heiser and Wilson C. Hsieh (Eds.). USENIX Association, 309\u2013318. https:\/\/www.usenix.org\/conference\/atc12\/technical-sessions\/presentation\/serebryany"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3122948.3122949"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250770"},{"key":"e_1_3_2_52_2","unstructured":"Julien Signoles. 2018. From Static Analysis to Runtime Verification with Frama-C and E-ACSL. https:\/\/tel.archives-ouvertes.fr\/tel-04469397"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3464974.3468451"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.29007\/FPDH"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2015.7054186"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632911"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704879","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704879","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:33Z","timestamp":1770200313000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704879"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":56,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704879"],"URL":"https:\/\/doi.org\/10.1145\/3704879","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}