Recent News
Inaugural School of Engineering Teaching Innovation Fellows selected
February 2, 2024
UNM computer scientist wins NSF CAREER Award to optimize supercomputer performance
February 1, 2024
Hand and Machine Lab’s Experimental Clay Exhibition closing celebration Nov. 17
November 15, 2023
Moses selected as special assistant to the dean for educational initiatives
October 3, 2023
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.