An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR
AProVE is a powerful termination prover for various programming languages, including a termination analysis method for imperative programs specified in the LLVM intermediate representation (IR). The method internally works in three steps: first, it transforms LLVM IR code into a symbolic execution graph; second, the graph is translated into an integer transition system; finally, termination of the transition system is proved by the back end of AProVE.
Since AProVE is unverified software, our aim is to increase its reliability by certifying the generated proofs.· To this end, we require formal semantics of all program representations, i.e., for LLVM IR, for symbolic execution graphs and for integer transition systems. As the latter is already available, we define the former ones. We note that our semantics for LLVM IR use arithmetic with unbounded integers. We further verify the first and the second step of AProVE’s termination method, including verified algorithms to check concrete proofs. Since the third step can already be certified, we obtain a complete formally verified method for certifying AProVE’s termination proofs of LLVM IR programs. The whole formalization has been done in Isabelle/HOL and our certifier is available as a Haskell program via code generation.
Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:45 - 17:30
Rewriting and Automated ReasoningCPP at CPP
Chair(s): Cyril Cohen Université Côte d’Azur, Inria, France
Streamed session: https://youtu.be/TVqCuMMTuos?t=2806
|A Modular Isabelle Framework for Verifying Saturation Provers|
Sophie Tourret Max Planck Institute for Informatics, Jasmin Blanchette Vrije Universiteit AmsterdamPre-print Media Attached
|An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR|
Max W. Haslbeck University of Innsbruck, René Thiemann University of InnsbruckPre-print Media Attached
|A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems|
Alexander Lochmann University of Innsbruck, Aart Middeldorp University of Innsbruck, Fabian Mitterwallner University of Innsbruck, Bertram FelgenhauerPre-print Media Attached