Recent News
Computer science student chosen for Churchill Scholarship
January 11, 2023
Leaving a legacy: Computer science professor’s research honored with Test of Time Award
December 9, 2022
Virtual workshop on climate-driven extreme events planned Nov. 10
October 25, 2022
MathWorks gives $2 million to UNM to create endowed chair for Department of Computer Science
October 18, 2022
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.