Skip to Content

Certification of Termination and Safety Proofs

Posted on

A number of incorrect proofs are revealed annually in the software verification competitions. Program analysis is a complex task, accomplished by modern program analyzers by translating imperative programs to an intermediate formal language. Certification research aims to increase the trustworthiness of such analyzers.

A common intermediate formal language is that of integer transition systems (ITSs), and common properties that are analyzed are termination and safety properties. For this reason, my certification research, conducted at the University of Innsbruck (UIBK) has taken this focus.

I worked on this project at as postdoctoral fellow in 2016 and 2017. Research in this direction is ongoing at the UIBK, the project page can be found here. The research has furthered development of the certification tool CeTA.