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.
BibTeX - Entry
@InProceedings{lammich:LIPIcs:2019:11077,
author = {Peter Lammich},
title = {{Generating Verified LLVM from Isabelle/HOL}},
booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
pages = {22:1--22:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-122-1},
ISSN = {1868-8969},
year = {2019},
volume = {141},
editor = {John Harrison and John O'Leary and Andrew Tolmach},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11077},
URN = {urn:nbn:de:0030-drops-110777},
doi = {10.4230/LIPIcs.ITP.2019.22},
annote = {Keywords: Isabelle/HOL, LLVM, Separation Logic, Verification Condition Generator, Code Generation}
}
|
Keywords: |
|
Isabelle/HOL, LLVM, Separation Logic, Verification Condition Generator, Code Generation |
|
Collection: |
|
10th International Conference on Interactive Theorem Proving (ITP 2019) |
|
Issue Date: |
|
2019 |
|
Date of publication: |
|
05.09.2019 |
|
Supplementary Material: |
|
http://www21.in.tum.de/~lammich/isabelle_llvm |
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)