Automated techniques and tools for analysis, verification, testing, and synthesis are indispensable in ensuring that today’s very complex software systems (e.g., operating systems, database management systems, or control systems of embedded or industrial systems) behave as intended, are resilient to vulnerabilities and exploitation, and are as efficient as possible, reducing the needed energy consumption. The current techniques and tools face significant challenges in scalability and precision. The scalability of precise techniques is not sufficient for truly large-scale digital systems, such as complex software applications or intricate controller designs. Scalable techniques often lack precision (e.g. produce false positives/negatives verification results or produce programs/controllers that do not behave optimally). This leads to developer productivity loss or costly errors in digital systems. This gap hinders the seamless integration of digital technologies into various sectors, including critical infrastructure and autonomous systems. In addition to the scalability-precision gap, there are other challenges such as: i) assumption of the complete code or model, ii) interaction between high-level and low-level code or iii) complex system specification. Finally, the relationship between the techniques and tools to be used for developing SW and economics is fundamental because the costs associated with obtaining and using the needed tools and the benefits produced must be carefully balanced. However, questions on the economic impacts of defects and vulnerabilities present in software and the costs of removing such defects are often shelved due to insufficient data.
VASSAL project addresses these challenges by the joint research agenda performed in four areas: (i) Logics and Automata, (ii) Model-based Design, Analysis and Synthesis (MBD), (iii) Automated analysis and verification on the source code level, and (iv) Economic assessment and implications.
