2026-08-10T13:30:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11077 2024-03-06T10:47:18Z ddc:004 open_access

Generating Verified LLVM from Isabelle/HOL Lammich, Peter Isabelle/HOL LLVM Separation Logic Verification Condition Generator Code Generation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Peter Lammich 2019 Is Part Of LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2019.22 urn:nbn:de:0030-drops-110777 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.22 eng https://creativecommons.org/licenses/by/3.0/legalcode