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.