BEGIN:VCALENDAR
VERSION:1.0
PRODID:Faculty of Science and Engineering - Research
BEGIN:VEVENT
SUMMARY:Theory Seminar: Algorithms for Checking Infinite Descent
DESCRIPTION;ENCODING=QUOTED-PRINTABLE: This week Theory meeting  will have an invited speaker (hosted by Fred), details below.=0D=0A=
=0D=0A=
Speaker: Reuben Rowe (Royal Holloway)=0D=0A=
=0D=0A=
Title: Algorithms for Checking Infinite Descent=0D=0A=
=0D=0A=
Abstract:=0D=0A=
=0D=0A=
The (PSPACE-complete) Infinite Descent property underpins the trace-based validation of cyclic derivations that capture inductive and coinductive reasoning, as well as the size-change approach to proving program termination. In the literature, we find a couple of different algorithms described for deciding Infinite Descent: a dynamic programming algorithm incorporating a fixed-point saturation (e.g. as suggested in the size-change termination paper by Lee, Jones, and Ben-Amram), and an encoding via containment of omega automata (e.g. in Brotherston's thesis).=0D=0A=
=0D=0A=
In this talk I will describe work in which we have developed an alternative automata-theoretic encoding and an optimisation of the dynamic programming algorithm that takes into account some specific symmetries present in the Infinite Descent problem. I will also describe some more efficient, but approximate (i.e. incomplete) approaches for checking Infinite Descent that we have developed. I will comment on the relative tradeoffs in the (runtime) complexity of the decision procedures, and report on an experimental evaluation of our implementations of these algorithms within the Cyclist theorem prover framework. Interestingly, we found the approximate methods to provide good coverage in practice. I will also mention some work on formalising these criteria for Infinite Descent within the Isabelle theorem prover.=0D=0A=
=0D=0A=
 =0D=0A=
=0D=0A=
 
LOCATION:Room 4.24. Peter Landin Building, Mile End. E1 4NS
DTSTART:20260501T150000
DTEND:20260501T170000
END:VEVENT
END:VCALENDAR