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 03451

Applied Deductive Verification

( Nov 02 – Nov 07, 2003 )

(Click in the middle of the image to enlarge)

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

Organizers



Summary

Software and hardware systems are increasingly employed in safety or mission critical applications. Deductive verification can be used during development to minimize the risk of their failure. Although the costs associated with verification are often considered high, verification methods have achieved considerable success and there is increasing industrial interest in applying such methods.

The aim of this Dagstuhl seminar was to bring together researchers from academia and industry who are applying deduction to substantial "real-world" problems. We interpret deduction in a broad sense including interactive and automated theorem proving, model checking, program analysis, and the use of decision procedures. Deductive verification is the application of these methods to system analysis; its scope ranges from using theorem provers to carry out full-scale system verification to more light-weight applications that are easier to automate, such as analyzing system properties using model checkers or other decision procedures. Topics relevant for the seminar included research on:

  • promising application-oriented foundations,
  • method combination (e.g., integrating deduction and model checking), and
  • abstraction and other techniques that can reduce the complexity of verification problems.

Applications include:

  • Software verification, including protocols, concurrent systems, multimedia applications, and security,
  • Hardware verification, including pipelined architectures and cache protocols as well as parameterized verification, and
  • Tool verification, i.e., the verification of tools used in safety critical application, such as hardware-targeted compilers.

During the seminar we aimed to achieve a cross-fertilization between theoreticians and practitioners working in the area. This was achieved both by overview talks on the state of the art in the application of deductive methods, and by providing a forum for communication between researchers working on theory with practitioners from industry who are applying verification tools to large-scale applications. The seminar also featured evening tutorials and tool demonstrations.


Scientific Highlights

Formal techniques are increasingly being used to tackle `real-world' industrial applications, and several speakers provided evidence of this. For example, Thomas Arts gave a fascinating overview of formal verification activity at Ericsson, while Patrick Cousot discussed a rigorous proof that the avionics software used in current Airbus aircraft cannot encounter floating-point overflows.

While we have not yet reached the stage of being able to perform a complete verification of large systems, we have many examples of proving either `big properties of small systems' or `small properties of big systems'. Indeed, we can see complete formal verification as one end of a continuum with traditional forms of static checking (type checking etc.) at the other. Thomas Ball and Sriram Rajamani discussed the impressive success of the SLAM static checker, using theorem proving technology to enhance static checking, which apparently identifies a productive point on this continuum.

One key technique for tackling large and complex problems is abstraction , and several speakers discussed the use of abstract interpretation in this capacity. Another powerful technique in real-world problem solving is the identification of certain canonical classes of problems into which many others can be mapped (e.g. propositional satisfiability, linear or semidefinite programming). Armin Biere's talk suggested that quantified boolean formulas (QBF) may become such a class in the near future.

Meanwhile, steady progress on more traditional fronts was reported. For example, Harald Rueß discussed the current techniques and progress made for combining decision procedures for quantifier-free theories, and Ken McMillan surveyed his key idea of using interpolants to allow bounded model checking to be used for complete correctness verification, not merely bug-finding.

A full description of the participants and talks may be found at the list of talks. Slides for many of the talks can also be found at this address.


Participants
  • André Arnold (University of Bordeaux, FR)
  • Thomas Arts (IT University of Göteborg, SE) [dblp]
  • Thomas Ball (Microsoft Research - Redmond, US) [dblp]
  • David Basin (ETH Zürich, CH) [dblp]
  • Armin Biere (Universität Linz, AT) [dblp]
  • Patrick Cousot (ENS - Paris, FR) [dblp]
  • Radhia Cousot (Ecole Polytechnique - Palaiseau, FR)
  • Harald Ganzinger (MPI-SWS - Saarbrücken, DE)
  • Hubert Garavel (INRIA - Grenoble, FR) [dblp]
  • Alain Griffault (University of Bordeaux, FR)
  • John R. Harrison (Intel - Hillsboro, US) [dblp]
  • Holger Hermanns (Universität des Saarlandes, DE) [dblp]
  • Hardi Hungar (Universität Oldenburg, DE) [dblp]
  • Warren A. Hunt (University of Texas - Austin, US)
  • Dieter Hutter (DFKI - Saarbrücken, DE)
  • Patrick Maier (MPI für Informatik - Saarbrücken, DE)
  • Kenneth McMillan (Cadence Labs - Berkeley, US) [dblp]
  • J Strother Moore (University of Texas - Austin, US) [dblp]
  • Martijn Oostdijk (Radboud University Nijmegen, NL)
  • Wolfgang J. Paul (Universität des Saarlandes, DE) [dblp]
  • Lawrence Paulson (University of Cambridge, GB) [dblp]
  • Doron A. Peled (University of Warwick - Coventry, GB) [dblp]
  • Mark Pichora (MPI für Informatik - Saarbrücken, DE)
  • Amir Pnueli (New York University, US)
  • Andreas Podelski (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Sriram K. Rajamani (Microsoft Research - Redmond, US) [dblp]
  • Harald Ruess (SRI - Menlo Park, US) [dblp]
  • Andrey Rybalchenko (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Mooly Sagiv (Tel Aviv University, IL) [dblp]
  • Peter H. Schmitt (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Johann M. Schumann (NASA / RIACS - Moffett Field, US)
  • Bernhard Steffen (TU Dortmund, DE) [dblp]
  • Marten Van Hulst (Philips Research Europe - Eindhoven, NL)
  • Uwe Waldmann (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Reinhard Wilhelm (Universität des Saarlandes, DE) [dblp]
  • Greta Yorsh (Tel Aviv University, IL) [dblp]
  • Lenore D. Zuck (University of Illinois - Chicago, US) [dblp]