VASSAL logo

Verification and Analysis for Safety and Security of Applications in Life

Automated analysis and verification on the source code level

Motivation

Current formal analysis and verification methods often suffer scalability and/or precision issues. Moreover, applicability of these approaches in practice is frequently hindered by their inability to handle incomplete code (i.e., code fragments), while developers are reluctant to write verification harnesses for their code. At the same time, a need for further development of new verification techniques stems from constant arrival of new programming and specification languages and techniques, lately often involving AI-based methods.

Strategic goals

Leader


Florian Zuleger
TUW

BUT

  • Tomáš Vojnar
  • Adam Rogalewicz
  • Tomáš Dacík

TUW

  • Georg Weissenbacher
  • Florian Zuleger

CEA

  • Allan Blanchard
  • Julien Signoles

HISRO

  • Tomáš Kratochvíla