Dagstuhl Seminar 14351
Decision Procedures and Abstract Interpretation
( Aug 24 – Aug 29, 2014 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/14351
Organizers
- Daniel Kroening (University of Oxford, GB)
- Thomas W. Reps (University of Wisconsin - Madison, US)
- Sanjit A. Seshia (University of California - Berkeley, US)
Coordinator
- Aditya Thakur (University of Wisconsin - Madison, US)
Contact
- Christina Schwarz (for administrative matters)
Schedule
The purpose of the seminar is to bring together members of two communities:
- the community that designs and implements abstract interpreters;
- the community that designs and implements decision procedures (particularly for use in SMT solvers).
These communities have several interests in common. In particular, the analysis tools that are created by members of each community can be viewed as using symbolic techniques to explore the state space of a transition system. Both areas have a long history. However, the respective repertoires of techniques used in the two disciplines are quite different, and each community has its own mindset and outlook. Recently, some ideas and methods have appeared that demonstrate new connections between the two disciplines, which suggests that the time is ripe for a meeting to promote cross-fertilization between the areas at a deep technical level.
Because the topics to be discussed during the seminar concern the core "analysis engines" used inside tools for hardware verification, software verification, and tools for identifying software defects, a hoped-for outcome of the seminar is that the participants will be equipped to improve the technology used in such tools. Even modest advances in technology could have immediate applications in tools such as Microsoft's SLAM tool (and other similar tools for finding defects), and thereby have a significant impact on the computing experience of hundreds of millions of people worldwide.
Some of the issues that will be addressed during the seminar are
- The use of logic to support abstract interpretation.
- The use of abstract interpretation to implement better decision procedures.
- The design of decision procedures for logics extended with fixed-point operators.
- The use of decision-procedure-like refinements in program-analysis algorithms.
The seminar will be held concurrently with a second seminar entitled "Next Generation Static Software Analysis Tools" (Dagstuhl Seminar 14352). The two seminars will be coordinated to some degree. The invitation lists will be disjointed, but it is likely that at least one joint activity will be carried out during the week.
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
- Aws Albarghouthi (University of Toronto, CA) [dblp]
- Joshua Berdine (Microsoft Research UK - Cambridge, GB) [dblp]
- Martin Brain (University of Oxford, GB) [dblp]
- Jörg Brauer (Verified Systems International GmbH - Bremen, DE) [dblp]
- Alessandro Cimatti (Bruno Kessler Foundation - Trento, IT) [dblp]
- Vijay D'Silva (Google - San Francisco, US) [dblp]
- Bruno Dutertre (SRI - Menlo Park, US) [dblp]
- Alberto Griggio (Bruno Kessler Foundation - Trento, IT) [dblp]
- Arie Gurfinkel (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Julien Henry (VERIMAG - Grenoble, FR) [dblp]
- Jacob Howe (City University - London, GB) [dblp]
- Daniel Kroening (University of Oxford, GB) [dblp]
- Akash Lal (Microsoft Research India - Bangalore, IN) [dblp]
- Antoine Miné (ENS - Paris, FR) [dblp]
- Ruzica Piskac (Yale University, US) [dblp]
- Blanc Regis (EPFL - Lausanne, CH)
- Thomas W. Reps (University of Wisconsin - Madison, US) [dblp]
- Michel Rueher (University of Nice, FR) [dblp]
- Peter Schrammel (University of Oxford, GB) [dblp]
- Sanjit A. Seshia (University of California - Berkeley, US) [dblp]
- Rahul Sharma (Stanford University, US) [dblp]
- Rohit Sinha (University of California - Berkeley, US) [dblp]
- Aditya Thakur (University of Wisconsin - Madison, US) [dblp]
- Charlotte Truchet (University of Nantes, FR) [dblp]
- Thomas Wies (New York University, US) [dblp]
- Hongseok Yang (University of Oxford, GB) [dblp]
- Florian Zuleger (TU Wien, AT) [dblp]
Classification
- programming languages / compiler
- verification / logic
Keywords
- program analysis
- abstract interpretation
- abstract domain
- fixed-point finding
- satisfiability checking
- satisfiability modulo theories
- decision procedures
