Verification and Analysis for Safety and Security of Applications in Life

Widening ParticipationHORIZON-CSAID: 101160022
EC Contribution
€14,999
Consortium Size
5 orgs
Start Year
2024
Summary

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.

Consortium (5)

Project Results (13)

Source: CORDIS, the EU research results database.

Publications (9)
A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators
ACM Transactions on Embedded Computing Systems· 2025DOI
Beatrice Melani, Ezio Bartocci, Michele Chiari
Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration
Lecture Notes in Computer Science, Programming Languages and Systems· 2025DOI
Florian Sextl, Adam Rogalewicz, Tomáš Vojnar, Florian Zuleger
RacerF: Data Race Detection with Frama-C (Competition Contribution)
Lecture Notes in Computer Science, Tools and Algorithms for the Construction and Analysis of Systems· 2025DOI
Tomáš Dacík, Tomáš Vojnar
Regular Grammars for Sets of Graphs of Tree-Width 2
2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)· 2025DOI
Marius Bozga, Radu Iosif, Florian Zuleger
Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs
Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence· 2025DOI
Maris F. L. Galesloot, Roman Andriushchenko, Milan Ceska, Sebastian Junges, Nils Jansen
Small Decision Trees for MDPs with Deductive Synthesis
Lecture Notes in Computer Science, Computer Aided Verification· 2025DOI
Roman Andriushchenko, Milan Češka, Sebastian Junges, Filip Macák
Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation
Lecture Notes in Computer Science, Tools and Algorithms for the Construction and Analysis of Systems· 2025DOI
David Chocholatý, Vojtěch Havlena, Lukáš Holík, Jan Hranička, Ondřej Lengál, Juraj Síč
Decentralized Planning Using Probabilistic Hyperproperties
Pontiggia F., Macák F., Andriushchenko R., Chiari M., Češka M.
RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)
Tomáš Dacík ORCID-Logo, Tomáš Vojnar ORCID-Logo
Deliverables (4)