Sarah Winkler receives Doc-fForte scholarship   (26 February 2010)

For her PhD project in the area of automated reasoning, Sarah Winkler was awarded a three year doc-fForte grant by the Austrian Academy of Sciences.

Although the foundations of computers rely on the logical principles, logical reasoning, i.e., the ability to draw conclusions from certain facts, is something they have yet to be taught. The research area of automated reasoning deals with the development of respective software systems, which is also the topic of this PhD project.

Sarah did both her bachelor and master studies in computer science at the University of Innsbruck. When graduating in 2008, she received a "Studienförderpreis des Deutschen Freundeskreises der Universitäten Innsbrucks" for her academic achievements, in particular her master thesis on "Termination Tools in Knuth-Bendix Completion". In February 2009 she won a PhD scholarship out of the "Nachwuchsförderung" provided by the LFU Innsbruck. Recently, she was awarded a doc-fForte grant which allows her to continue her PhD for three more years.

Dealing with automated reasoning, Sarah's topic is in a field receiving increasing interest. The development of sophisticated automated reasoning and theorem proving systems promoted a variety of applications in computer science and mathematics. For example, theorem provers are by now widely used to formally verify hardware components such as computer chips. This approach became particularly common when in 1994 a bug in the FDIV unit of Intel processors led to a uniquely expensive recall. Also quality assurance of software systems takes advantage of formal verification techniques. Especially in safety critical applications, they provide a means to guarantee that all required specifications are met. Likewise, cryptographic protocols such as Needham-Schröder and Kerberos or Smart Card Protocols can be verified using methods from the area of automated reasoning. Mathematical research benefits from automated reasoning techniques as well. For example, the use of theorem provers resulted in considerable contributions in the area of algebraic structures such as groups and lattices. Also proof assistants such as Isabelle or Coq became popular in various areas of mathematics, as they allow to formally capture and prove mathematical statements.

Many algorithms underlying automated reasoning systems are described by rule sets called deduction calculi. Most of these calculi require an ordering as ingredient. The choice of this parameter is crucial for successful computations but hard to determine appropriately in advance.

In her PhD project, Sarah aims at designing automated reasoning calculi which avoid this critical parameter by employing automatic termination tools instead. Both the theoretical foundations and implementation techniques underlying automatic termination provers have been advanced significantly over the last decade, thereby fostering the development of powerful and efficient termination tools such as TTT2.

Thus the employment of termination provers in deduction calculi allows for novel implementations of automated reasoning systems. Providing more flexibility than conventional tools relying on standard orderings, these new systems are assumed to solve input problems which could not be handled before. When combined with the simulation of multiple parallel processes, the success rate can be further increased.

In her master project, Sarah already investigated this approach for the Knuth-Bendix completion calculus. This classical automated reasoning method can be viewed as a generalization of Buchberger's algorithm to compute Gröbner bases for polynomial ideals, developed in 1965 by Prof. Bruno Buchberger in Innsbruck. Implemented in the tool mkbTT, the new Knuth-Bendix completion approach indeed proved to solve input problems which could not be cracked by established methods, such as problems from the mathematical field of group theory.

In a PhD project supervised by Prof. Aart Middeldorp, Sarah will continue to pursue this line of research. Initially, the developed software is to be further advanced concerning efficiency and success rate. In the sequel, the developed approach is to be extended to other automated deduction calculi, for example to prove inductive theorems. After establishing respective theoretical foundations, the developed methods are to be implemented. The corresponding tools can then be evaluated concerning their applicability to practical problems.

Since security is a growing issue, formal verification is naturally a research area becoming more and more important. By exploring possible enhancements of automated reasoning calculi, this project strives to contribute to this trend by advancing the foundations of respective formal verification tools.

Links:

• OeAW
• mkbTT