24.08.14 - 29.08.14, Seminar 14351

Decision Procedures and Abstract Interpretation

Diese Seminarbeschreibung wurde vor dem Seminar auf unseren Webseiten veröffentlicht und bei der Einladung zum Seminar verwendet.

Motivation

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

  1. The use of logic to support abstract interpretation.
  2. The use of abstract interpretation to implement better decision procedures.
  3. The design of decision procedures for logics extended with fixed-point operators.
  4. 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.