Certification of Termination and Safety Proofs

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.

Relevant publications include:

• A Formalization of the LLL Basis Reduction Algorithm
• A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
• A verified LLL algorithm
• A verified factorization algorithm for integer polynomials with polynomial complexity
• Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper)
• Certifying safety and termination proofs for integer transition systems
• Subresultants
• A formalization of the Berlekamp-Zassenhaus factorization algorithm
• CeTA–Certifying Termination and Complexity Proofs in 2016
• A Formalization of Berlekamp’s Factorization Algorithm
• Algebraic Numbers in Isabelle/HOL