The Complex(ity) Landscape of Checking Infinite Descent

Explore a comprehensive analysis of cyclic proof systems and the complexity of checking Infinite Descent in this 18-minute conference talk from POPL 2024. Delve into the study of criteria for Infinite Descent in an abstract, logic-independent setting, focusing on Büchi automata encodings and relational abstractions. Examine the parameterized time complexities of these criteria in relation to key dimensions of cyclic proofs, including the number of vertices in proof-tree graphs and vertex width. Discover novel algorithms that improve upon existing parameterized complexity approaches. Learn about the implementation of studied criteria and their performance comparison across various benchmarks. Gain insights into the promising field of automatic verification through cyclic proof systems, where induction is managed implicitly.

[POPL'24] The Complex(ity) Landscape of Checking Infinite Descent