3rd German Verification Day 2007, July 1, Berlin


The two German top projects on verification and analysis of embedded systems, the DFG funded long-term research project AVACS, a Transregional Collaborative Research Center (SFB/TR), and the BMBF funded applied research project Verisoft, are presenting selected results from their research, within the third German Verification Day, on July 1, 2007, in Berlin, Germany. Whereas AVACS´ research challenge is of foundational nature, developing novel verification algorithms covering the design space of complex embedded systems, Verisoft´s challenge is to achieve fully verified components for industry-critical systems, employing state-of-art automatic and interactive verification tools.

The foundational project AVACS combines the expertise in formal verification at its three sites Freiburg, Oldenburg, and Saarbrücken to address the rigorous mathematical analysis of models of complex safety critical computerized systems, such as aircrafts, trains, cars, or other artifacts, whose failure can endanger human life. AVACS aims at raising the state of the art in automatic verification and analysis techniques of such complex systems from its current level of applicability to isolated points in the design space of such systems to a level allowing a comprehensive, holistic, and ultimately automatic verification of such systems, with research activities structured into three key project areas, addressing verification of real-time systems, hybrid systems, and holistic system verification, respectively.

The Verisoft project (www.verisoft.de) combines the expertise of key industrial (BMW, Infineon, T-Systems) and academic teams to achieve fully verified key application components, covering the full design layer from applications to hardware, strengthening the competitive positioning in the addressed industrial sectors by being able to offer fully formally verified components. To this end, formal mathematical proofs will be rigorously established using a combination of state-of-the-art interactive and automatic verification methods.


Time Program
0900 - 0930 Invited Talk:
Wolfram Schulte (Microsoft Research): A Glimpse of a Verifying C Compiler
0930 - 1000 Andre Platzer (Universität Oldenburg): Differential Logic for Reasoning about Hybrid Systems
1000 - 1030 Bernhard Beckert (Uni Koblenz): tba.
1030 - 1100 Coffee Break
1100 - 1130 Andrey Rybalchenko (MPI/EPFL): Termination Proofs for C0 Programs
1130 - 1200 Henning Burchardt (Universität Oldenburg): Fully Automated Stability Verification for Piecewise Affine Systems
1200 - 1230 Stefan Disch, (Universität Freiburg): Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets.
1230 - 1400 Lunch Break
1400 - 1430 Dirk Leinenbach (DFKI): Compiler Verification in Context of Pervasive System Verification
1430 - 1500 Felix Klaedtke (ETH Zürich): Don't Care Words with Application to the Automata-based Approach for Real Addition
1500 - 1530 Alex Krauss (TU München): Partial Recursive Functions in Higher Order Logic

1530 - 1600 Coffee Break
1600 - 1630 Sebastian Borgan (Universität Saarbrücken): The Verisoft Academic System Demonstrator
1630 - 1700 Christoph Scholl (Universität Freiburg): Automatic Verification of Hybrid Systems with Large Discrete State Space

Location and Registration

GVD 2007 is co-located and affiliated with CAV 2007 in Berlin. CAV 2007 will be held at the Park-Inn Hotel Alexanderplatz.

Registration fee for GVD 2007 only is 90 Euros until June, 15. Please register on CAV's official registration page.


There will be no proceedings for this workshop.

Revision 29 Jun 2007