-
Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation
Logic Specification into Conventional Workflows.
Zain K Aamer1, Rini Banerjee1, Hiroyuki Katsura1, David
Kaloper-Meršinjak1, Dimitrios J. Economou, Kayvan Memarian, Dhruv
Makwana, Neel Krishnaswami, Benjamin C. Pierce, Christopher Pulte, and Peter
Sewell.
Proc. ACM Program. Lang., 10(PLDI), June 2026.
1 these authors contributed equally.
[ bib |
doi |
pdf |
http |
abstract ]
-
Fulminate: Testing CN Separation-Logic Specifications in
C.
Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte,
Neel Krishnaswami, and Peter Sewell.
In POPL 2025.
[ bib |
doi |
pdf |
abstract ]
-
CN: Verifying systems C code with separation-logic
refinement types.
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian,
Peter Sewell, and Neel Krishnaswami.
In POPL 2023, Proc. ACM Programming Languages 7, POPL, Article 1.
[ bib |
doi |
project page |
pdf |
abstract ]