License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.22
URN: urn:nbn:de:0030-drops-110777
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11077/
Go to the corresponding LIPIcs Volume Portal

Lammich, Peter

Generating Verified LLVM from Isabelle/HOL

pdf-format:
LIPIcs-ITP-2019-22.pdf (0.5 MB)

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI