The Speakers

Cyclic reasoning, in which induction is managed implicitly, is a promising approach to automatic verification. The soundness of cyclic proof graphs is ensured by checking them against a trace-based Infinite Descent property.  While deciding Infinite Descent is PSPACE-complete in general, its cost varies sharply with two natural parameters: the number of graph vertices and the vertex-width that bounds the components tracked simultaneously. To gain speed in practice, one can trade completeness for efficiency. Cyclone follows this strategy: it layers several fast, but necessarily incomplete, semi-decision procedures for Infinite Descent atop a complete exponential fallback. These alternative algorithms are developed and benchmarked, and Cyclone is shown to deliver substantial runtime gains on real workloads. 

This talk outlines the theoretical landscape as well as the practical improvements and their empirical impact. We also briefly reflect on how we, as researchers, can use Infinite Descent for managing the inherently (often frustrating) cyclic nature of research itself.