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

We present a formalization in Isabelle/HOL of a comprehensive framework for proving the completeness of automatic theorem provers based on resolution, superposition, or other saturation calculi. The framework helps calculus designers and prover developers derive, from the completeness of a calculus, the completeness of prover architectures implementing the calculus. It also helps derive the completeness of calculi obtained by lifting ground (i.e., variable-free) calculi. As a case study, we re-verified Bachmair and Ganzinger’s resolution prover RP to show the benefits of modularity.

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:45 - 17:30
Rewriting and Automated ReasoningCPP at CPP
Chair(s): Cyril CohenUniversité 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 TourretMax Planck Institute for Informatics, Jasmin BlanchetteVrije 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. HaslbeckUniversity of Innsbruck, René ThiemannUniversity 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 LochmannUniversity of Innsbruck, Aart MiddeldorpUniversity of Innsbruck, Fabian MitterwallnerUniversity of Innsbruck, Bertram Felgenhauer
Pre-print Media Attached