News

FWF project accepted   (1 March 2010)

In its last assembly on March 1 the FWF board accepted Univ.-Prof. Dr. Aart Middeldorp's project proposal "Confluence: Automation, Certification, Extensions". Confluence is a fundamental property in computer science. If an algorithm has the confluence property then computations have unique results.

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 Univ.-Prof. Middeldorp to strengthen its excellent international cooperations with Japan, The Netherlands, and Germany.

Univ.-Prof. Middeldorp has already led a successful FWF project (Termination Tools: Verification and Optimization) on another important property of algorithms: termination. An algorithm terminates if it always returns a result within finite time. Termination is essential for proving that programs meet their specification. In this project an internationally acclaimed tool TTT2 for automatically proving termination of algorithms has been developed. To avoid bugs the output of TTT2 is machine-certified with the help of the higher-order theorem prover Isabelle/HOL.

For the new project on confluence the recent results achieved for termination are essential. Within the next three years an automated tool for checking confluence of algorithms will be developed. Another main aim is to machine-certify the output of confluence provers, something which no one has attempted before.

Links: