You are here: Home Research Research Cluster AVACS - Automatic Verification and Analysis of Complex Systems
Document Actions

AVACS - Automatic Verification and Analysis of Complex Systems

Automatic Verification and Analysis of Complex Systems (SFB/TR 14, 2003-2015)

avacsThe Transregional Collaborative Research Center AVACS is based on a joint venture and partnership between the Universities of Freiburg, Oldenburg and Saarbrücken and the Max Planck Institut für Informatik in Saarbrücken. It is funded by the German Research Foundation (DFG). In Freiburg, we support this project with our research and expertise in computer architecture, operating systems, software engineering, and artificial intelligence.

The vision of AVACS encompasses the comprehensive formal verification of safety-critical systems. More precisely, AVACS concentrates on the verification of safety-critical systems controlling and interacting with physical and technical processes. These systems can be found in everyday life, and are prevalent for example in the transportation sector (cars, trains and planes).
The failure or incorrect operation of safety-critical systems can put human lives in danger. While limiting the potential damage of these systems is one alternative, a better approach would be to prevent these systems from failing altogether. The ability and tools needed to automatically verify such complex systems have traditionally been very limited, meaning only certain aspects or parts of each system could be analysed and checked.

Leveraging the complementary research skills of all three sites allows AVACS to combine multiple basic verification algorithms for modelling and analysing the full complexity of these safety-critical systems. AVACS also strives to achieve a high degree of automation in this verification process. We exploit domain-specific knowledge to develop customized analysis techniques and efficient decision procedures. Using heuristic-based approaches we combine knowledge and techniques from multiple fields into a holistic verification approach.

The working groups based in Freiburg are involved in all three project areas of AVACS: real-time systems, hybrid systems and coarse-grained system structure.

Prof. Dr. Bernd Becker, Department of Computer Science


Personal tools