Generating Verified LLVM from Isabelle/HOL

Peter Lammich

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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
Original languageEnglish
Title of host publicationITP 2019: Interactive Theorem Proving
Publication statusAccepted/In press - 1 Jun 2019
EventInteractive Theorem Proving - Portland, United States
Duration: 8 Sept 201913 Sept 2019
https://itp19.cecs.pdx.edu/

Conference

ConferenceInteractive Theorem Proving
Abbreviated titleITP 2019
Country/TerritoryUnited States
CityPortland
Period8/09/1913/09/19
Internet address

Keywords

  • Isabelle/HOL
  • LLVM
  • Separation Logic
  • Verification condition generator
  • Code generation

Fingerprint

Dive into the research topics of 'Generating Verified LLVM from Isabelle/HOL'. Together they form a unique fingerprint.

Cite this