POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Wed 17 Jan 2024 15:50 - 16:10 at Kelvin Lecture - Automata And Complexity Chair(s): Fritz Henglein

Cyclic proof systems, in which induction is managed implicitly, are a promising approach to automatic verification. The soundness of cyclic proof graphs is ensured by checking them against a trace-based Infinite Descent property. Although the problem of checking Infinite Descent is known to be PSPACE-complete, this leaves much room for variation in practice. Indeed, a number of different approaches are employed across the various cyclic proof systems described in the literature. In this paper, we study criteria for Infinite Descent in an abstract, logic-independent setting. We look at criteria based on Büchi automata encodings and relational abstractions, and determine their parameterized time complexities in terms of natural dimensions of cyclic proofs: the numbers of vertices of the proof-tree graphs, and the vertex width—an upper bound on the number of components (e.g., formulas) of a sequent that can be simultaneously tracked for descent. We identify novel algorithms that improve upon the parameterised complexity of the existing algorithms. We implement the studied criteria and compare their performance on various benchmarks.

Wed 17 Jan

Displayed time zone: London change

15:10 - 16:30
Automata And ComplexityPOPL at Kelvin Lecture
Chair(s): Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital
15:10
20m
Talk
Parikh's Theorem Made Symbolic
POPL
Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS
15:30
20m
Talk
Efficient Matching of Regular Expressions with Lookaround Assertions
POPL
Konstantinos Mamouras Rice University, Agnishom Chattopadhyay Rice University
15:50
20m
Talk
The Complex(ity) Landscape of Checking Infinite Descent
POPL
Liron Cohen Ben-Gurion University of the Negev, Adham Jabarin Ben Gurion University, Andrei Popescu University of Sheffield, Reuben N. S. Rowe Royal Holloway University of London
16:10
20m
Talk
Positive Almost-Sure Termination – Complexity and Proof Rules
POPL