August 24 – 29 , 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)

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 4, Issue 8 Dagstuhl Report
Aims & Scope
List of Participants
Dagstuhl Seminar Schedule [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.

Summary text license
  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


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).

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.


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