Dagstuhl Seminar 09411
Interaction versus Automation: The two Faces of Deduction
( Oct 04 – Oct 09, 2009 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/09411
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)
Contact
- Annette Beyer (for administrative matters)
Schedule
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)
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.
- Franz Baader (TU Dresden, DE) [dblp]
- Domagoj Babic (Synopsys Inc. - Mountain View, US)
- Thomas Ball (Microsoft Corporation - Redmond, US) [dblp]
- Peter Baumgartner (NICTA - Canberra, AU) [dblp]
- Bernhard Beckert (Universität Koblenz-Landau, DE) [dblp]
- Nikolaj S. Bjørner (Microsoft Corporation - Redmond, US) [dblp]
- Maria Paola Bonacina (University of Verona, IT) [dblp]
- Richard Bubel (Chalmers UT - Göteborg, SE) [dblp]
- Michael Codish (Ben Gurion University - Beer Sheva, IL) [dblp]
- Carsten Fuhs (RWTH Aachen, DE) [dblp]
- Ulrich Furbach (Universität Koblenz-Landau, DE) [dblp]
- Jürgen Giesl (RWTH Aachen, DE) [dblp]
- Georges Gonthier (Microsoft Research UK - Cambridge, GB) [dblp]
- Reiner Hähnle (Chalmers UT - Göteborg, SE) [dblp]
- Thomas C. Hales (University of Pittsburgh, US) [dblp]
- Krystof Hoder (University of Manchester, GB)
- Ranjit Jhala (University of California - San Diego, US) [dblp]
- Deepak Kapur (University of New Mexico - Albuquerque, US) [dblp]
- Vladimir Klebanov (Universität Koblenz-Landau, DE) [dblp]
- Laura Kovács (ETH Zürich, CH) [dblp]
- Alexander Krauss (TU München, DE)
- Viktor Kuncak (EPFL - Lausanne, CH) [dblp]
- Assia Mahboubi (Ecole Polytechnique - Palaiseau, FR) [dblp]
- Claude Marché (University of Paris South XI, FR) [dblp]
- Aart Middeldorp (Universität Innsbruck, AT) [dblp]
- Wojciech Mostowski (Radboud University Nijmegen, NL) [dblp]
- Tobias Nipkow (TU München, DE) [dblp]
- Michael Norrish (NICTA - Canberra, AU) [dblp]
- Albert Oliveras (Polytechnic University of Catalonia, ES) [dblp]
- Wolfgang J. Paul (Universität des Saarlandes, DE) [dblp]
- Brigitte Pientka (McGill University - Montreal, CA) [dblp]
- André Platzer (Carnegie Mellon University, US) [dblp]
- Zvonimir Rakamaric (University of British Columbia - Vancouver, CA) [dblp]
- Albert Rubio (UPC - Barcelona, ES) [dblp]
- Andrey Rybalchenko (MPI-SWS - Saarbrücken, DE) [dblp]
- Renate Schmidt (University of Manchester, GB) [dblp]
- Manfred Schmidt-Schauss (Universität Frankfurt, DE) [dblp]
- Peter H. Schmitt (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Peter Schneider-Kamp (University of Southern Denmark - Odense, DK) [dblp]
- Gert Smolka (Universität des Saarlandes, DE) [dblp]
- Viorica Sofronie-Stokkermans (MPI für Informatik - Saarbrücken, DE) [dblp]
- Kurt Stenzel (Universität Augsburg, DE)
- Aaron Stump (University of Iowa - Iowa City, US) [dblp]
- Laurent Théry (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
- René Thiemann (Universität Innsbruck, AT) [dblp]
- Christian Urban (TU München, DE) [dblp]
- Andrei Voronkov (University of Manchester, GB) [dblp]
- Christoph Walther (TU Darmstadt, DE)
- Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]
- Benjamin Weiß (KIT - Karlsruher Institut für Technologie, DE)
- Makarius Wenzel (TU München, DE) [dblp]
- Freek Wiedijk (Radboud University Nijmegen, NL) [dblp]
Related Seminars
- Dagstuhl Seminar 9310: Deduction (1993-03-08 - 1993-03-12) (Details)
- Dagstuhl Seminar 9512: Deduction (1995-03-20 - 1995-03-24) (Details)
- Dagstuhl Seminar 9709: Deduction (1997-02-24 - 1997-02-28) (Details)
- Dagstuhl Seminar 99091: Deduction (1999-02-28 - 1999-03-05) (Details)
- Dagstuhl Seminar 01101: Deduction (2001-03-04 - 2001-03-09) (Details)
- Dagstuhl Seminar 03171: Deduction and Infinite-state Model Checking (2003-04-21 - 2003-04-25) (Details)
- Dagstuhl Seminar 05431: Deduction and Applications (2005-10-23 - 2005-10-28) (Details)
- Dagstuhl Seminar 07401: Deduction and Decision Procedures (2007-09-30 - 2007-10-05) (Details)
- Dagstuhl Seminar 13411: Deduction and Arithmetic (2013-10-06 - 2013-10-11) (Details)
- Dagstuhl Seminar 15381: Information from Deduction: Models and Proofs (2015-09-13 - 2015-09-18) (Details)
- Dagstuhl Seminar 17371: Deduction Beyond First-Order Logic (2017-09-10 - 2017-09-15) (Details)
- Dagstuhl Seminar 19371: Deduction Beyond Satisfiability (2019-09-08 - 2019-09-13) (Details)
- Dagstuhl Seminar 21371: Integrated Deduction (2021-09-12 - 2021-09-17) (Details)
- Dagstuhl Seminar 23471: The Next Generation of Deduction Systems: From Composition to Compositionality (2023-11-19 - 2023-11-24) (Details)
- Dagstuhl Seminar 26091: Revisiting the Foundations of Deduction in a New World (2026-02-22 - 2026-02-27) (Details)
