http://www.dagstuhl.de/09411

October 4 – 9 , 2009, Dagstuhl Seminar 09411

Interaction versus Automation: The two Faces of Deduction

Organizers

Thomas Ball (Microsoft Corporation – Redmond, US)
Jürgen Giesl (RWTH Aachen, DE)
Reiner Hähnle (Chalmers UT – Göteborg, SE)
Tobias Nipkow (TU München, DE)


For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Seminar Proceedings DROPS
List of Participants
Dagstuhl Seminar Schedule [pdf]

Press Review

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.

Dagstuhl Seminar Series

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.