Recent News
UNM student creates game-changing in-seat food delivery service
April 1, 2025
Dissertation defense, April 7: Ala Jararweh
March 31, 2025
Dissertation defense, April 4: John Ringer
March 31, 2025
Computer Science Colloquium will discuss the use of AI in cyber-physical systems
March 27, 2025
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.