Document Open Access Logo

Generating Verified LLVM from Isabelle/HOL

Author Peter Lammich



PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.22.pdf
  • Filesize: 0.5 MB
  • 19 pages

Document Identifiers

Author Details

Peter Lammich
  • The University of Manchester, UK

Acknowledgements

We thank Maximilian P. L. Haslbeck and Simon Wimmer for proofreading and useful suggestions.

Cite AsGet BibTex

Peter Lammich. Generating Verified LLVM from Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 22:1-22:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.22

Abstract

We present a framework to generate verified LLVM programs from Isabelle/HOL. It is based on a code generator that generates LLVM text from a simplified fragment of LLVM, shallowly embedded into Isabelle/HOL. On top, we have developed a separation logic, a verification condition generator, and an LLVM backend to the Isabelle Refinement Framework. As case studies, we have produced verified LLVM implementations of binary search and the Knuth-Morris-Pratt string search algorithm. These are one order of magnitude faster than the Standard-ML implementations produced with the original Refinement Framework, and on par with unverified C implementations. Adoption of the original correctness proofs to the new LLVM backend was straightforward. The trusted code base of our approach is the shallow embedding of the LLVM fragment and the code generator, which is a pretty printer combined with some straightforward compilation steps.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Logic and verification
  • Theory of computation → Separation logic
Keywords
  • Isabelle/HOL
  • LLVM
  • Separation Logic
  • Verification Condition Generator
  • Code Generation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail