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 need to provide formal specifications of systems and requirements
• The limited algorithmic scalability, despite some impressive applications

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:

1. Efficient and scalable algorithms for automated verification and refinement of design models
2. Effective and efficient algorithms to automate the verification of actual software
3. Algorithms to synthesize control strategies, software components, or specifications

Ad 1. We will build on current expertise in model checking and automated theorem proving. Example research challenges in this area include:

• Extend model checking to infinite state systems (real-time, probabilistic, hybrid, or parametric)
• Develop compositional methods and parallel algorithms for model checking and refinement checking
• Raise the level of automation in refinement checking between models of different abstraction levels
• Complementary approaches: dynamic analysis, run-time verification and certified model checking

Ad 2. We will build on current expertise in static analysis, software model checking, and SMT solving. Example research challenges in this area include:

• Investigate (and extend where possible) the algorithmic limits in software model checking
• Analyze high-level programming language constructs or design patterns automatically
• Verify concurrent software, under various memory models and scheduling assumptions
• Verify distributed software, under various communication models and fault assumptions
• Verify quantitative properties, like real-time, information leakage, memory consumption

Ad 3. We mainly apply strategy synthesis methods from algorithmic game theory.
Example research challenges in this area include:

• Synthesize a set of constraints for which a parametric system satisfies its requirements
• Synthesize control strategies, test cases, or even software components from specifications
• Synthesize annotations in software, to facilitate refinement checking or program verification
• Synthesize secure protocols and strategies for multi-agent systems
• Inductive property synthesis from dynamic executions, e.g. invariant learning.

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.