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
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 06161

Simulation and Verification of Dynamic Systems

( Apr 17 – Apr 22, 2006 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:



Simulation is widely used for modeling engineering artifacts and natural phenomena to gain insight into the operation of those systems. Simulation, using a simulator or otherwise experimenting with fictitious situation can show the eventual real effects of some possible conditions. In contrast, formal verification is concerned with proving or disproving the correctness of a system with respect to a certain property, using mathematical and logical methods. Verification techniques include explicit-state enumeration, symbolic simulation, model checking, static program analysis, and theorem proving techniques.

Despite of these different objectives, the fields of simulation and verification address similar research challenges. In particular, the need for identifying and defining suitable models of the dynamic system under study unifies both research fields. Modeling methods have a significant impact on how easily certain phenomena can be described, they influence the acceptance in the application community and the possibilities to be analyzed and simulated. They formed one focus of discussion and the basis for a working group exploring the potentials and limitations of different modeling approaches. Although there are disparate approaches in the fields of simulation and verification for validating timed, probabilistic, and hybrid systems, both fields address component-based and abstraction-based validation techniques. Refinement and abstraction plays a crucial role, both in simulation and verification, but even more so if both approaches are combined. The role of refinement and abstractions has been a second focus of general discussion intensified in a dedicated working group. In application areas like embedded systems and systems biology, researchers of simulation and verifi- cation are coming together to see a lot of common problems and interesting solutions that help propelling research in the respective areas. During the seminar, the application area of Systems Biology moved quickly into the focus of interest, which resulted in a working group addressing the question whether the application area of systems biology requires specific modeling, simulation, and verification tools, and how biological systems differ from engineered ones.

The dialog between the simulation and verification community about the abovementioned issues most notably started with the Computational Methods in Systems Biology Workshop series, the first of which took place in Trento in 2003. The Dagstuhl Seminar continued and intensified this dialog between both communities working on simulating and verifying dynamic systems.


Dagstuhl is dedicated to working groups. In contrast to traditional conference settings, the schedule offered plenty of time for working groups, discussions, and spontaneous activities. To give an overview about the different areas, state-of-the-art plenary talks were given in the beginning of the seminar. Short presentations provided the opportunity for each participant to present and discuss his or her own work during the morning session. The afternoons were dedicated to working groups. The themes of the working groups formed during the first days of the seminar. In the evening, the results of the working groups were presented in plenary sessions.

Intertwining working groups and plenary sessions helped to work on concrete questions in the different groups and to support a cross fertilization among them. The seminar was a truly interdisciplinary event and all participants played an active role in driving the progress and content of the seminar and the individual working groups. Their results took shape in three documents that formed the basis of the included working groups’ report The challenge of combining simulation and verification. As always, Schloss Dagstuhl and its ambiance, its unusual blend of the old with the new, the organization, and the very helpful staff contributed largely to the success of the seminar.

  • Gregory Batt (Boston University, US) [dblp]
  • Luca Bortolussi (University of Udine, IT) [dblp]
  • Jeremy T. Bradley (Imperial College London, GB) [dblp]
  • Luca Cardelli (Microsoft Research UK - Cambridge, GB) [dblp]
  • Matteo Cavaliere (Microsoft Research - University Trento, IT) [dblp]
  • Roland Ewald (Universität Rostock, DE)
  • François Fages (INRIA - Le Chesnay, FR) [dblp]
  • Holger Hermanns (Universität des Saarlandes, DE) [dblp]
  • Jane Hillston (University of Edinburgh, GB) [dblp]
  • Hardi Hungar (OFFIS - Oldenburg, DE) [dblp]
  • Peter Kemper (TU Dortmund, DE)
  • Jörg Kreiker (Universität des Saarlandes, DE)
  • Céline Kuttler (Interdisciplinary Research Institute - Lille, FR)
  • Mila Majster-Cederbaum (Universität Mannheim, DE) [dblp]
  • Alke Martens (Universität Rostock, DE) [dblp]
  • Pieter J. Mosterman (The MathWorks Inc. - Natick, MA USA, US) [dblp]
  • David M. Nicol (University of Illinois - Urbana Champaign, US) [dblp]
  • Flemming Nielson (Technical University of Denmark - Lyngby, DK) [dblp]
  • Holger Pfeifer (Universität Ulm, DE)
  • Henrik Pilegaard (Technical University of Denmark - Lyngby, DK)
  • Stefan Ratschan (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Hanne Riis Nielson (Technical University of Denmark - Lyngby, DK) [dblp]
  • Sean Sedwards (Università di Trento, IT) [dblp]
  • Oleg Sokolsky (University of Pennsylvania - Philadelphia, US) [dblp]
  • Helena Szczerbicka (Leibniz Universität Hannover, DE) [dblp]
  • Boleslaw Szymanski (Rensselaer Polytechnic Institute - Troy, US)
  • Adelinde M. Uhrmacher (Universität Rostock, DE) [dblp]
  • Silke Wagner (MPI für Informatik - Saarbrücken, DE)
  • Oskar Wibling (Uppsala University, SE)
  • Reinhard Wilhelm (Universität des Saarlandes, DE) [dblp]
  • Verena Wolf (Universität des Saarlandes, DE) [dblp]