Effective automated software verification : a multilayered approach
- Blicha, Martin
- Sharygina, Natasha (Degree supervisor)
- Kofroň, Jan (Degree supervisor)
- 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.
- Collections
- Language
-
- English
- Classification
- Computer science and technology
- License
- License undefined
- Open access status
- green
- Identifiers
-
- NDP-USI 2023INF002
- ARK ark:/12658/srd1326721
- URN urn:nbn:ch:rero-006-121643
- Persistent URL
- https://n2t.net/ark:/12658/srd1326721
Statistics
Document views: 67
File downloads:
- 2023INF002.pdf: 96