Society is increasingly depending on the proper functioning of its ICT infrastructure. This applies both to the civil society (e.g. power distribution, traffic regulation, social networks), to industry (robots, 3D printing, logistics), as well as to our individual environment (social networks, cars, IoT devices). This imposes high standards on software quality, in particular for safety-critical and business-critical applications. Formal verification has matured over the last decade as a methodology to prove that a software system satisfies its requirements. It is a rigorous method, based on principles of mathematical logic. However, its widespread application is still hindered by two main obstacles:
The mission of the work package is to increase the quality of software-intensive systems, by enabling the large-scale application of automated verification and synthesis. This can be achieved by improving the algorithms themselves, by automating labor-intensive parts of interactive methods, and by developing strategies for the gradual introduction of verification methods in the software development process. We are driven by challenging research questions, with the aim to understand, develop and apply:
Ad 1. We will build on current expertise in model checking and automated theorem proving. Example research challenges in this area include:
Ad 2. We will build on current expertise in static analysis, software model checking, and SMT solving. Example research challenges in this area include:
Ad 3. We mainly apply strategy synthesis methods from algorithmic game theory.
Example research challenges in this area include:
The AU DIGIT work package on Automated Verification and Synthesis will organize activities in order to provide a platform for inspiring scientific collaboration between the contributing groups; to reach out to (local) industry for the purpose of dissemination, inspiration and collaboration; and to identify complementary strengths to write successful project applications.