Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 17:00 - 17:15 at CPP - Rewriting and Automated Reasoning Chair(s): Cyril Cohen

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 Jan

Displayed 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

16:45
15m
Talk
A Modular Isabelle Framework for Verifying Saturation Provers
CPP
Sophie Tourret Max Planck Institute for Informatics, Jasmin Blanchette Vrije Universiteit Amsterdam
Pre-print Media Attached
17:00
15m
Talk
An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR
CPP
Max W. Haslbeck University of Innsbruck, René Thiemann University of Innsbruck
Pre-print Media Attached
17:15
15m
Talk
A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
CPP
Alexander Lochmann University of Innsbruck, Aart Middeldorp University of Innsbruck, Fabian Mitterwallner University of Innsbruck, Bertram Felgenhauer
Pre-print Media Attached