A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems (CPP 2021 - Certified Programs and Proofs)

Write a Blog >>

Sun 17 - Fri 22 January 2021 Online

Who

Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer

Track

CPP 2021

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Tue 19 Jan 2021 17:15 - 17:30 at CPP - Rewriting and Automated Reasoning Chair(s): Cyril Cohen

Abstract

The first-order theory of rewriting is a decidable theory for finite left-linear right-ground rewrite systems. We present a formally verified variant of the decision procedure for the class of linear variable-separated rewrite systems. This variant supports a more expressive theory and is based on the concept of anchored ground tree transducers. The correctness of the decision procedure is formalized in Isabelle/HOL.

Link to Preprint

http://cl-informatik.uibk.ac.at/software/fortissimo/cpp2021/paper.pdf

Alexander Lochmann

University of Innsbruck

Aart Middeldorp

University of Innsbruck

Fabian Mitterwallner

University of Innsbruck

Bertram Felgenhauer

Long presentation

Short presentation

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

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