 Internal
Auf Deutsch, Bitte!
|
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
|
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.
|
