News Archives

Proving Termination Automatically By Dependency Pairs

March 1, 2005

  • Date: Tuesday, March 1, 2005 
  • Time: 11:00 a.m. 
  • Place: Woodward 149

Juergen Giesl <giesl@informatik.rwth-aachen.de> 
RWTH Aachen Germany Termination is a fundamental property of programs and the proof of termination is an important task in program verification. Since verification is usually very costly, our goal is to automate this task as much as possible.

This talk presents the dependency pair approach, which is one of the most powerful techniques for automated termination proofs. After introducing the basic ideas of this approach, we present several recent improvements which considerably reduce and simplify the constraints produced for termination proofs. Moreover, we show how the indeterminisms and search problems of the dependency pair approach can be mechanized efficiently. We implemented our results in the automated termination prover AProVE and evaluated them on large collections of examples.

The talk is based on joint work with Thomas Arts, Rene Thiemann, Pete Schneider-Kamp, and Stephan Falke.