TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 06172

Directed Model Checking

( Apr 26 – Apr 29, 2006 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/06172

Organizers




Summary

Model checking is an increasingly popular verification technology in software and hardware systems analysis. While model checking was originally devised as a complete state space exploration technique aiming at proving models correct, its current primary use is in debugging systems by locating errors in the state space of the model. In particular in explicit-state model checking, which is often used in model checking software systems, debugging is aided by the ease with which offending system traces, also referred to as counterexamples, can be made available. Counterexamples which are system traces leading from the initial state to a property-violating state and their analysis often hints at the causes of errors.

The sheer size of the reachable state space of realistic models imposes tremendous challenges on the algorithmics underlying model checking technology. A complete exploration of the state space is often infeasible and approximations are needed. This has lead to a large body of research on optimizing the performance of model checking, including abstraction techniques, state space reduction techniques and improvements in the algorithmics of model checking.

To this end, a recent development was to reconcile model checking with heuristics guided search strategies well investigated in the area of artificial intelligence, in particular in action planning. In standard model checking, the selection of a successor node is performed in a naive fashion without taking knowledge about the problem structure into account. In action planning there is a long tradition of using heuristics guided informed search algorithms, such as A*, in the search for a state in which a planning goal has been reached. The artificial intelligence community has a long and impressive line of research in developing and improving search algorithms over very large state spaces under a broad range of assumptions. It has therefore been observed that there are many similarities between model checking and action planning as well as a large potential for synergies when reconciling these domains, see for instance the discussions at the Dagstuhl seminar 01451 Exploration of Large State Spaces. Even though directed model checking approaches have been developed for symbolic and explicit-state model checking, the most natural match seems to be between heuristics guided state space search and explicit state model checking.

The seminar brought together researchers from the system verification and the artificial intelligence domains in order to discuss the current state of the art, and to elicit and discuss research challenges and future directions. The current state of the art was documented by presentations given by the participants, which we briefly summarize in Section 2. The definition of research challenges was the goal of working groups that met during off-hour breakout sessions.

The seminar succeeded in documenting the state of the art in Directed Model Checking as well as defining challenges for future research. A number of publications have since emerged from the seminar. Amongst others, a paper by Dwyer, Person and Elbaum that was based a presentation during the seminar was awarded the Best Paper Award at the Foundations of Software Engineering conference held in Portland in the Fall of 2006.

The seminar was held in the fabulous atmosphere that Dagstuhl has offered to the scientific community for more than a decade. We thank the Dagstuhl board and staff for their hospitality. The format of the seminar was that of a more unusual 3 day duration. The participants regretted the relative scarcity of time and agreed that a 5 day duration would have facilitated and enhanced the work of the working groups.


Participants
  • Husain Aljazzar (Universität Konstanz, DE)
  • Nina Amla (Cadence - Sunnyvale, US)
  • Cyrille Artho (National Institute of Informatics - Tokyo, JP) [dblp]
  • Markus Bauhan (Universität Konstanz, DE)
  • Dragan Bosnacki (TU Eindhoven, NL) [dblp]
  • Chandrasekhar Boyapati (Univ. of Michigan - Ann Arbor, US)
  • Alessandro Cimatti (Centro Ricerche FIAT - Trento, IT) [dblp]
  • Henning Dierks (OFFIS - Oldenburg, DE)
  • Klaus Dräger (Universität des Saarlandes, DE)
  • Matthew Dwyer (University of Nebraska - Lincoln, US) [dblp]
  • Stefan Edelkamp (TU Dortmund, DE) [dblp]
  • Ansgar Fehnker (NICTA - Sydney, AU)
  • Bernd Finkbeiner (Universität des Saarlandes, DE) [dblp]
  • Wolfgang Grieskamp (Microsoft Research - Redmond, US) [dblp]
  • Malte Helmert (Universität Freiburg, DE) [dblp]
  • Shahid Jabbar (TU Dortmund, DE)
  • Sebastian Kupferschmid (Universität Freiburg, DE)
  • Johannes Leitner (Universität Konstanz, DE)
  • Stefan Leue (Universität Konstanz, DE) [dblp]
  • Tilman Mehler (TU Dortmund, DE)
  • Eric Mercer (Brigham Young Univ., US)
  • Bernhard Nebel (Universität Freiburg, DE) [dblp]
  • Charles Pecheur (University of Louvain, BE)
  • Suzette Person (University of Nebraska - Lincoln, US) [dblp]
  • Theo Ruys (University of Twente, NL)
  • Viktor Schuppan (Trento Povo, IT)
  • Maria Luisa Villani (Univ. of Sannio - Benevento, IT)
  • Willem Visser (NASA / RIACS - Moffett Field, US) [dblp]
  • Anton Wijs (CWI - Amsterdam, NL) [dblp]

Classification
  • Verification/Logic
  • Artificial Intelligence
  • Sofware-Engineering
  • Heuristics/Evolutionary Algorithms
  • Data Structures/Algorithms/Complexity

Keywords
  • Model Checking
  • Artificial Intelligence
  • AI Plannning
  • Guided Traversal
  • State Explosion Problem
  • Error Detection
  • Protocol Analysis
  • Hardware and Software Verification and Validation
  • Heuristics
  • Evaluation Functions
  • Relaxations
  • Lower Bounds
  • Pattern Databases
  • Abstractions
  • Heuristic Search (Best-First Search
  • A*
  • IDA*
  • etc.)
  • Local Search (Hill-Climbing
  • Genetic Algorithms
  • etc.)
  • Symbolic Heuristic Search (BDDA*
  • ADDA*
  • SetA*
  • SA* etc.)
  • Byte-Code and Object-Code Verification
  • I/O Efficient Search
  • Symmetry Reduction
  • Partial-Order Reduction
  • Search Space Partitioning
  • Bounded Model Checking