24. – 29. August 2014, Dagstuhl-Seminar 14351

Decision Procedures and Abstract Interpretation


Daniel Kroening (University of Oxford, GB)
Thomas W. Reps (University of Wisconsin – Madison, US)
Sanjit A. Seshia (University of California – Berkeley, US)


Aditya Thakur (University of Wisconsin – Madison, US)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 4, Issue 8 Dagstuhl Report
Gemeinsame Dokumente
Programm des Dagstuhl-Seminars [pdf]


The abstract interpretation (AI) and decsion procedure (DP) communities have several interests in common. Tools created by each of these communities can be viewed as using symbolic techniques to explore the state state of a transition system. However, the respective repertoires of techniques used in the two disciplines are quite different, and each community has its own mindset and outlook. The seminar sought to capitalize on recent ideas that demonstrated new connections between the two disciplines, and, consequently, promote the cross-fertilization between the areas at a deep technical level.

The seminar had 27 participants from both the AI and DP communities. To keep pariticipants from both areas engaged during a session, the organizers refrained from filling a session only with talks focusing on a particular community. Instead, each session consisted of talks by participants of both research communities. Furthermore, talks by young researchers were scheduled earlier in the week, which enabled them to get better feedback on their research.

The Dagstuhl Seminar 14352 "Next Generation Static Software Analysis Tools" was held concurrently with Dagstuhl Seminar 14351. There were a number of joint activities organized to foster interaction among participants of the two seminars:

  • The first session on Monday was a joint session for participants of both seminars. In this session, all participants introduced themselves and briefly described their research interests. Furthermore, Patrick Cousot, an organizer for Seminar 14352, and Thomas Reps, an organizer for Seminar 14351, each gave a "scene-setting" talk.
  • The Wednesday excursion to the steel mill and Egyptian exhibit was organized as a joint activity.
  • A joint session was organized on Thursday afternoon. The talks in this session were given by participants of both seminars.
  • The seating arrangement for the Friday dinner was organized so that participants from both seminars sat together.
  • The schedule of talks for both seminars was shared with all participants. Hence, participants of one seminar were able to attend a specific talk in the other seminar, if they felt the talk was especially relevant.

Apart from the planned activities listed above, the week saw a lot of informal discussions among participants of these two seminars in the evenings.

The seminar also featured talks about two other research areas: constraint programming (CP) and machine learning (ML). The talks by Mine, Rueher, and Truchet highlighted the use of abstract interpretation in CP. The talks by Reps, Seshia, Sharma, and Thakur discussed the application of ML techniques, such as inductive learning, to problems in AI and DP. Both these sets of talks garnered interesting discussions about the connections among all these various reseach areas. Furthermore, this discussion indicates that future seminars should include even more researchers and practitioners from not just the AI and DP communities, but also the CP and ML communities.

  Creative Commons BY 3.0 Unported license
  Daniel Kroening and Thomas W. Reps and Sanjit A. Seshia and Aditya V. Thakur


  • Programming Languages / Compiler
  • Verification / Logic


  • Program analysis
  • Abstract interpretation
  • Abstract domain
  • Fixed-point finding
  • Satisfiability checking
  • Satisfiability modulo theories
  • Decision procedures


Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.