Doctoral thesis

Effective automated software verification : a multilayered approach

  • 2022

PhD: Università della Svizzera italiana

English Automated software verification decides correctness of a given program with respect to a given formal specification. Formal verification techniques based on model checking provide the necessary guarantees by exploring program’s behaviour exhaustively and automatically. Even though the general problem that automated software verification is trying to solve is undecidable, it is quite efficient on many instances that arise in practice. However, significant challenges related to scalability persist for complex modern programs. In our work, we argue that this task can be approached by providing solutions at different levels, which we identify as foundational, verification and cooperative layers of the problem. These correspond to decision and interpolation procedures, sequential model-checking algorithms, and multi-agent solving approaches. We further argue that working on the higher layers can significantly benefit from a deep understanding of the layers beneath them. Overall, we advance the field of automated software verification by contributing solutions on all three layers.
  • English
Computer science and technology
License undefined
Open access status
Persistent URL

Document views: 18 File downloads:
  • 2023INF002.pdf: 15