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 06081

Software Verification: Infinite-State Model Checking and Static Program Analysis

( Feb 19 – Feb 24, 2006 )


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

Organizers



Summary

Software systems are present at the very heart of many daily-life applications, such as in communication (telephony and mobile Internet), transportation, energy, health, etc. Such systems are very often critical in the sense that their failure can have considerable human/economical consequences. Therefore, there is a real need of rigorous and automated approaches for software development which guarantee a high level of reliability. It is widely admitted that to ensure reliability, development methods must include algorithmic analysis and verification techniques which allow one (1) to detect automatically defective behavior of the system and to analyze its source, and (2) to check that every component of a system conforms to its specification, that is to establish automatically its correctness.

For modern software systems, many complex aspects are of crucial importance such as manipulation of data over unbounded domains (integers, reals, etc.), object-orientation, dynamic memory structures (creation of objects, pointer manipulation), dynamic control (multi-threading, procedure calls), synchronization between concurrent processes, parameterization, real-time and hybrid modeling, etc. The development of software analysis and verification methods and tools allowing to deal efficiently with such aspects constitutes a major scientific and technological challenge. Two important and quite active research communities are particularly concerned with this challenge: the community of computer-aided verification, especially the community of (infinite-state) model checking, and the community of static program analysis. The two communities have adopted different approaches: The model-checking community studies complete methods for the verification analysis of abstract models. These abstract models may involve infinity features such as those mentioned above. On the other hand, the program analysis community works with approximate analyses applied on formalisms that are closer to programming languages and specification formalisms used in practice.

While the approaches and the developed techniques are different, the two communities share a common mathematical background and their methods are based on common basic concepts and principles: transition systems and automata based models, abstractions, fixpoint computations, reachability analysis based on symbolic representation structures of (potentially infinite) sets of configurations, etc.

About the Seminar

Dagstuhl Seminar 06081 ``Software Verification: Infinite-State Verification and Static Program Analysis'' brought together 51 researchers from these two communities in order to (1) improve and deepen the mutual understanding of the developed technologies, (2) compare these technologies and identify complementary aspects, and (3) trigger collaborations leading to new developments. The seminar was held from February 19 to February 24, 2006, at the International Conference and Research Center for Computer Science Schloss Dagstuhl, Germany. The participants came from 12 countries, mainly from Europe and the US. More specifically, 1 participant came from Austria, 2 from Belgium, 1 from The Czech Republic, 1 from Denmark, 12 from France, 12 from Germany, 3 from Israel, 1 from Italy, 1 from Russia, 2 from Switzerland, 5 from the United Kingdom, and 10 from the United States.

In 31 talks, the participants presented results of their recent research. These talks touched many issues of automatic software verification including: abstraction techniques, invariant generation, termination analysis, automata-based representation structures and applications of regular model checking, analysis of pointer and heap structures, timed and hybrid systems, multi-threaded programs, parameterized systems, probabilistic models and verification methods, etc.

In a final session on Friday morning, the participants discussed how to progress further in the field of automatic software verification and how to get the developed technology to practice. Lack of common benchmarks and notations and a tendency to evaluate techniques on academic toy examples rather than on real code (e.g., from Java libraries) were identified as obstacles to fair comparison of different analyses and broader dissemination of the results. Reasons for this are that the area is quite broad with many different aspects, and that some of the techniques are still in an experimental stage.

During the evenings and nights, the great facilities of Dagstuhl offered plenty of opportunities to enjoy other pleasures besides science, among them beer, cheese, and music (in alphabetical order). On Wednesday afternoon there was an opportunity to join an excursion to Luxembourg city.


Participants
  • Eugene Asarin (University Paris-Diderot, FR) [dblp]
  • Parosh Aziz Abdulla (Uppsala University, SE) [dblp]
  • Ittai Balaban (New York University, US)
  • Thomas Ball (Microsoft Research - Redmond, US) [dblp]
  • Dirk Beyer (EPFL - Lausanne, CH) [dblp]
  • Ahmed Bouajjani (University Paris-Diderot, FR) [dblp]
  • Patrick Cousot (ENS - Paris, FR) [dblp]
  • Radhia Cousot (Ecole Polytechnique - Palaiseau, FR)
  • Giorgio Delzanno (University of Genova, IT) [dblp]
  • Dino Distefano (Queen Mary University of London, GB) [dblp]
  • Javier Esparza (Universität Stuttgart, DE) [dblp]
  • Kousha Etessami (University of Edinburgh, GB) [dblp]
  • Cormac Flanagan (University of California - Santa Cruz, US) [dblp]
  • Martin Fränzle (Universität Oldenburg, DE) [dblp]
  • Peter Habermehl (University Paris-Diderot, FR) [dblp]
  • Radu Iosif (VERIMAG - Grenoble, FR) [dblp]
  • S. Purush Iyer (North Carolina State University - Raleigh, US)
  • Yan Jurski (University Paris-Diderot, FR)
  • Jens Knoop (TU Wien, AT) [dblp]
  • Barbara König (Universität Stuttgart, DE) [dblp]
  • Jörg Kreiker (Universität des Saarlandes, DE)
  • Julia Lawall (University of Copenhagen, DK) [dblp]
  • Axel Legay (University of Liège, BE) [dblp]
  • Jérôme Leroux (University of Bordeaux, FR) [dblp]
  • Martin Leucker (TU München, DE) [dblp]
  • Alexander Malkis (MPI für Informatik - Saarbrücken, DE)
  • Richard Mayr (North Carolina State University - Raleigh, US) [dblp]
  • Antoine Miné (ENS - Paris, FR) [dblp]
  • Markus Müller-Olm (Universität Münster, DE) [dblp]
  • Joel Ouaknine (University of Oxford, GB) [dblp]
  • Shaz Qadeer (Microsoft Research - Redmond, US) [dblp]
  • Alexander Rabinovich (Tel Aviv University, IL) [dblp]
  • Jean-Francois Raskin (Free University of Brussels, BE) [dblp]
  • Thomas W. Reps (University of Wisconsin - Madison, US) [dblp]
  • Peter Revesz (University of Nebraska - Lincoln, US)
  • Andrey Rybalchenko (MPI-SWS - Saarbrücken, DE) [dblp]
  • Mooly Sagiv (Tel Aviv University, IL) [dblp]
  • David Schmidt (Kansas State University, US)
  • Philippe Schnoebelen (ENS - Cachan, FR) [dblp]
  • Stefan Schwoon (Universität Stuttgart, DE)
  • Nassim Seghir (MPI für Informatik - Saarbrücken, DE)
  • Helmut Seidl (TU München, DE) [dblp]
  • Nikolay Shilov (Russian Academy of Sc. - Novosibirsk, RU)
  • Mihaela Sighireanu (University Paris-Diderot, FR) [dblp]
  • Henny Sipma (Stanford University, US)
  • Tayssir Touili (University Paris-Diderot, FR)
  • Helmut Veith (TU München, DE) [dblp]
  • Tomas Vojnar (Brno University of Technology, CZ) [dblp]
  • Andrei Voronkov (University of Manchester, GB) [dblp]
  • Reinhard Wilhelm (Universität des Saarlandes, DE) [dblp]
  • James Worrell (University of Oxford, GB) [dblp]
  • Greta Yorsh (Tel Aviv University, IL) [dblp]

Classification
  • Verification/logic
  • semantics/specification
  • programming languages/compilers

Keywords
  • Infinite-state systems
  • model checking
  • program analysis
  • software verification