Document Open Access Logo

Fractional Separation Logic in Isabelle LLVM

Author Peter Lammich

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.27.pdf
  • Filesize: 0.68 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Fractional Separation Logic
  • LLVM
  • verification
  • Isabelle

Metrics

Abstract

We present a shallow embedding of fractional separation logic in Isabelle/HOL, based on fractional separation algebras with unbounded fractions. To support flexible ownership splitting and recombination, we use nominal labels that enable systematic distribution and collection of fractional permissions across separating conjunctions.
The logic is integrated into a verification condition generator that automates substantial parts of fraction arithmetic and label reasoning, significantly reducing manual proof effort. As a backend, we connect the framework to Isabelle LLVM, enabling the verification of executable LLVM code.
As a case study, we verify a parallel matrix-vector multiplication. The example illustrates recursive reasoning, parallel writes to disjoint segments of the result vector, and shared read access to the input vector via fractional permissions.

Cite As Get BibTex

Peter Lammich. Fractional Separation Logic in Isabelle LLVM. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.27

Author Details

Peter Lammich
  • University of Twente, Enschede, The Netherlands

Funding

This work was supported by the NWO OCENW.M.21.291 "VESPA" grant.

Supplementary Materials

References

  1. Andrew W Appel. Program logics for certified compilers. Cambridge University Press, 2014. URL: http://www.cambridge.org/de/academic/subjects/computer-science/programming-languages-and-applied-logic/program-logics-certified-compilers?format=HB.
  2. Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. In Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '05, pages 259-270, New York, NY, USA, 2005. ACM. URL: https://doi.org/10.1145/1040305.1040327.
  3. John Boyland. Checking interference with fractional permissions. In Radhia Cousot, editor, Static Analysis, pages 55-72, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-44898-5_4.
  4. James Brotherston, Diana Costa, Aquinas Hobor, and John Wickerson. Reasoning over permissions regions in concurrent separation logic. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification, pages 203-224, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-53291-8_13.
  5. C. Calcagno, P.W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. In LICS 2007, pages 366-378, July 2007. URL: https://doi.org/10.1109/LICS.2007.30.
  6. Thibault Dardinier. Unbounded separation logic. Archive of Formal Proofs, September 2022. URL: https://www.isa-afp.org/entries/Separation_Logic_Unbounded.html.
  7. Thibault Dardinier, Peter Müller, and Alexander J. Summers. Fractional resources in unbounded separation logic. Proc. ACM Program. Lang., 6(OOPSLA2), October 2022. URL: https://doi.org/10.1145/3563326.
  8. Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller. Formal foundations for translational separation logic verifiers. Proc. ACM Program. Lang., 9(POPL), January 2025. URL: https://doi.org/10.1145/3704856.
  9. Vincent Jackson, Toby Murray, and Christine Rizkallah. A generalised union of rely-guarantee and separation logic using permission algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024), pages 23-1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.23.
  10. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of functional programming, 28:e20, 2018. URL: https://doi.org/10.1017/S0956796818000151.
  11. Steve Klabnik and Carol Nichols. The Rust Programming Language. No Starch Press, San Francisco, CA, USA, 2nd edition, 2022. Google Scholar
  12. Gerwin Klein, Rafal Kolanski, and Andrew Boyton. Mechanised separation algebra. In ITP, pages 332-337. Springer, August 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_22.
  13. Gerwin Klein, Rafal Kolanski, and Andrew Boyton. Separation algebra. Archive of Formal Proofs, May 2012. URL: https://www.isa-afp.org/entries/Separation_Algebra.shtml.
  14. Peter Lammich. Fractional Separation Logic in Isabelle LLVM. URL: https://github.com/lammich/IsaFracSep.
  15. Peter Lammich. Fractional Separation Logic in Isabelle LLVM. archived. URL: https://doi.org/10.5281/zenodo.20359872.
  16. Peter Lammich. Refinement to Imperative/HOL. In ITP, volume 9236 of LNCS, pages 253-269. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_17.
  17. Peter Lammich. Generating verified LLVM from Isabelle/HOL. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPIcs, pages 22:1-22:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.22.
  18. Peter Lammich. Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting. J. Autom. Reason., 68(3):14, 2024. URL: https://doi.org/10.1007/S10817-024-09701-W.
  19. Chris Lattner and Vikram Adve. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04), Palo Alto, California, March 2004. URL: https://doi.org/10.1109/CGO.2004.1281665.
  20. Xuan-Bach Le and Aquinas Hobor. Logical reasoning for disjoint permissions. In Amal Ahmed, editor, Programming Languages and Systems, pages 385-414, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-89884-1_14.
  21. Daniel Matichuk, Toby Murray, and Makarius Wenzel. Eisbach: A proof method language for isabelle. J. Autom. Reason., 56(3):261-282, March 2016. URL: https://doi.org/10.1007/s10817-015-9360-2.
  22. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  23. Peter W. O'Hearn. Resources, concurrency and local reasoning. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, pages 49-67, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-28644-8_4.
  24. Viktor Vafeiadis. Concurrent separation logic and operational semantics. Electron. Notes Theor. Comput. Sci., 276:335-351, September 2011. URL: https://doi.org/10.1016/j.entcs.2011.09.029.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact