Project Details

Verification and Analysis for Safety and Security of Applications in Life

Project Period: 1. 6. 2024 – 31. 5. 2027

Project Type: grant

Code: SEP-210979090

Agency: Evropská unie

Program: HORIZON EUROPE

Type
grant
Keywords

Formal methods, model-based-design, safety and security of software, economics of
software tools, software engineering

Abstract

VASSAL project focuses on leveraging the scientific excellence and innovation
capacity of the consortium in the field of software engineering to support safety
and security of digitised economies and societies. The key objective is to bring
together expertise of the consortium in specific domains to enhance and create
a new knowledge for robust and resilient SW engineering through scientific
strategy combining model-based design, formal methods and economics for
source-codes and systems.
As SW becomes more complex, ensuring its safety and
security (vulnerabilities free) becomes increasingly challenging and vital, not
only in safety-critical systems but across various operation systems and IoT as
well.
Formal methods and model-based design are taking an increasingly
significant role, building upon its already widespread use in safety-critical
applications, such as automotive or aerospace.  As basic building blocks in
engineering process, they enable to build robust and resilient SW and HW systems
(security-/safe-by-design) ensuring the reliability and correctness, leveraging
cybersecurity, and improving the development life-cycle, that lead to savings in
operational costs of systems.
The economic assessment and implications of
advanced SW engineering tools are not commonly available. VASSAL will deliver
a rare opportunity to explore and document the potential benefits of and
challenges in deployment in order to leverage the awareness and make inroads to
broader exploitation by end-users (especially SMEs) in segments, where these
issues are being overlooked due to the alleged non-returnability of the
investment.

Team members
Češka Milan, doc. RNDr., Ph.D. (DITS) – research leader
Andriushchenko Roman, Ing. (DITS)
Bobalová Martina, Mgr., Ph.D. (ÚI)
Dacík Tomáš, Ing. (DITS)
Doskočil Radek, doc. Ing., Ph.D., MSc (ÚI)
Fiedor Jan, Ing., Ph.D. (DITS)
Hudák David, Ing. (DITS)
Jírovec Martin, Ing. (DFIT-Dean)
Karas Michal, doc. Ing., Ph.D. (ÚF)
Křena Bohuslav, Ing., Ph.D. (DITS)
Lengál Ondřej, doc. Ing., Ph.D. (DITS)
Luhan Jan, Ing., Ph.D., MSc (ÚI)
Macák Filip, Ing. (DITS)
Novotná Veronika, doc. Mgr., Ph.D. (ÚI)
Širáňová Lenka, Ing., Ph.D. (ÚI)
Valko Roderik, MSc (DITS)
Veselá Sára, Ing.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Žižka Josef, Ing. (DCGM)
Publication Results

2025

  • ANDRIUSHCHENKO, R.; ČEŠKA, M.; JUNGES, S.; MACÁK, F. Small Decision Trees for MDPs with Deductive Synthesis. In Computer Aided Verification. Springer Cham, 2025. p. 169-192. ISBN: 978-3-031-98678-9. Detail
  • ANDRIUSHCHENKO, R.; ČEŠKA, M.; MACÁK, F.; FRANCESCO, P.; MICHELE, C. Decentralized Planning Using Probabilistic Hyperproperties. Proc. of the 24th International Conference on Autonomous Agents and Multiagent Systems. Detroit: 2025. p. 1688-1697. ISBN: 979-8-4007-1426-9. Detail
  • CHOCHOLATÝ, D.; HAVLENA, V.; HOLÍK, L.; HRANIČKA, J.; LENGÁL, O.; SÍČ, J. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. Proceedings of TACAS'25. Lecture Notes in Computer Science. Hamilton: Springer Verlag, 2025. no. 1, p. 23-44. ISSN: 0302-9743. Detail
  • DACÍK, T.; VOJNAR, T. RacerF: Data Race Detection with Frama-C (Competition Contribution). In Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 3. Lecture Notes in Computer Science. Hamilton: Springer Nature Switzerland AG, 2025. p. 248-253. ISBN: 978-3-031-90659-6. Detail
  • DACÍK, T.; VOJNAR, T. RacerF: Lightweight Static Data Race Detection for C Code. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. p. 37.1-37.19. ISBN: 978-3-95977-373-7. Detail
  • FLORIAN, S.; ROGALEWICZ, A.; VOJNAR, T.; ZULEGER, F. Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration. In Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025. Lecture Notes in Computer Science. Springer, 2025. p. 230-257. ISBN: 978-3-031-91121-7. Detail
  • GALESLOOT, M.; ANDRIUSHCHENKO, R.; ČEŠKA, M.; JUNGES, S.; JANSEN, N. Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization, 2025. p. 8518-8526. ISBN: 978-1-956792-06-5. Detail
Back to top