Interaction versus Automation: The two Faces of Deduction

Press Review

• Interaktion versus Automatisierung: Die zwei Gesichter der Deduktion.
  Wolfgang Back und Wolfgang Rudolph vom Computerclub Zwei im Gespräch mit Prof. Dr. Jürgen Giesl (Interiew ab 10:15 min)

Summary

Throughout the history of modern logic, there have been two strands of research: finding natural inference systems for a given problem domain and finding automatic procedures for solving specific logical problems. In computer science, these two strands became interactive and automated deduction. Powerful systems emerged in both camps (Coq, Isabelle, etc. versus Spass, Vampire, etc.), conferences were established, and separate communities developed.

However, none of the two kinds of systems were ideal for program verification. The interactive tools lacked the necessary automation and the automatic tools failed to cater for important aspects like arithmetic. And neither scaled well. Therefore a separate third, application-driven set of techniques and tools were developed. These are based on powerful automatic procedures for particular logical theories, ranging from propositional logic to arithmetic, and their combination, most notably in the form of SMT solvers. At the same time they were integrated with techniques from program analysis and automata theory. Again, a separate scientific community evolved.

Goals of the Seminar

There is clearly not just competition but also synergy among the three different approaches discussed in the previous section. For example, SMT solvers are successfully applied in program analysis and first-order provers are used in interactive systems. The KeY system is the result of combining an interactive approach to program verification with a high degree of automation. However, such combinations often raise questions and problems that require more interaction between the communities involved. These include

• exchange of formats for theories and proofs
• encoding of higher-order problems into first-order logic
• extension of automatic first-order provers with specific theories or abstraction techniques
• using automatic provers as servers that allow to incrementally add and delete formulas
• orchestration of interleaved automated and interactive inference
• rendering results of automated tools in human-readable form
• generation of proof certificates
• exploiting synergies between Abstract Interpretation and SMT solvers
• invariant inference, especially for quantified formulas
• exploiting program structure for efficient search
• test generation and support from SMT solvers
• programming language support for program analysis

The Dagstuhl seminar brought together the best researchers working on interactive and automatic deduction methods and tools, with a special emphasis on applications to program analysis and verification. In total we had 52 participants, mostly from Europe, but also from USA, Israel, and Australia. A good balance between more senior and junior participants was maintained. The program consisted of 39 relatively short talks, which gave ample time for discussion, both during and after the talks as well as during the meals and in the evenings. Altogether, we perceived the seminar as a very successful one, which allowed for cross-fertilization between research on interactive and on automated deduction. Moreover, it also helped to bridge gaps between foundational research on these topics and application-driven approaches; e.g., the transfer of new theoretical results into applications, or the discovery of new research problems motivated by applications.