Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


Proving Program Termination

  • Speaker:   Prof  Daniel Kroening  (University of Oxford)
  • Host:   Eva Navarro-Lopez
  • 23rd March 2011 at 14:15 in Lecture Theatre 1.4, Kilburn Building
Software bugs related to liveness can be particularly annoying; the program "gets stuck", and the user is left wondering whether it will resume responding.

Liveness-related bugs are therefore an important target for program analysis.

Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check is known to be the bottleneck of the procedure. We present an alternative algorithm that uses a light-weight check based on transitivity of ranking relations to prove program termination. We provide an experimental evaluation over a broad set of Windows drivers, and demonstrate that our algorithm is often able to conclude termination by examining only a small fraction of the program. As a consequence, our algorithm is able to outperform known approaches by multiple orders of magnitude.

The talk will contain some tutorial content on the state-of-the art techniques; no prior knowledge of termination analysis is assumed.
▲ Up to the top