Thursday, 16th of March 2017, 12:00 – 1:00

Certifying Complexity and Termination Proofs for Programs

SR 2, ICT Building,
Technikerstraße 21a, 6020 Innsbruck


Rene Thiemann
Associate Professor at CL group, University of Innsbruck


In recent years both the strength and the complexity of automated program analysis tools increased. Because of the latter, it regularly happens that some analysis is faulty.
In order to still maintain reliability we developed CeTA, a highly reliable and powerful certifier for (in)validating automatically generated complexity and termination proofs.
In the seminar we first present the general architecture of CeTA and then highlight some of recent challenges we had to solve for validating sophisticated complexity and termination proofs.