The automated termination and complexity analysis tool
AProVE
provides an implementation of many of the techniques discussed in this course.
For this course, the most convenient way to run AProVE is via its
Web Interface.
Further pointers
The course could not cover equivalence proving of programs
for time reasons. If you are interested in this topic, consider
watching the recording of my
talk on Proving Equivalence of
Imperative Programs via Constrained Rewriting Induction at the
Proof Systems for Mathematics and
Verification at EPFL in Lausanne in June 2024.
The course could not cover confluence analysis for time reasons.
Since 2012, there is the annual
Confluence Competition,
where tools for automated confluence analysis try to (dis)prove
confluence properties of input problems. There is also a
to the participation tools of this competition.