FWF project accepted   (28 June 2010)

In its last assembly on June 28, the FWF board accepted Dr. René Thiemann's project proposal "Improving Certifiers for Termination Proofs." Termination is a fundamental property in computer science, since it is essential for verifying the correctness of programs. If a program is terminating, then it always yields a result. There are several automated tools to check for termination. Those tools, however, are horrendously complex pieces of software. Hence, they may contain errors and thus report wrong results. To counteract this problem, recent achievements in automatically certifying such proofs have been made.

The Austrian Science Fund (FWF) is Austria's central funding organization for basic research. It orients itself on the standards of the international scientific community. The project supports a doctoral candidate and a postdoc researcher for three years, to gain valuable research experience on a high international level. Furthermore, it allows the team around Dr. Thiemann to strengthen the international cooperation with France and Germany.

In a precursor project of Univ.-Prof. Middeldorp a tool CeTA for automatic certification of termination proofs has been developed. The tool is a fully verified program, where all the necessary properties have been proven in the interactive theorem prover Isabelle/HOL. This includes an Isabelle formalization IsaFoR of the mathematical theory that is used in proving termination.

The new project on improving automatic certification of termination is based on the previous developments and aims at the following goals:

1. Increase the number of certifiable termination techniques.
2. Better integration of certifiers with termination tools.
3. Use certified proofs for establishing termination of Isabelle/HOL functions.
4. Certify complexity bounds of terminating functions.

Links:

• Computational Logic research group
• FWF
• Isabelle/HOL
• IsaFoR/CeTA