Model-Based Program Verification

Wytse Oortwijn

Software has integrated deeply into modern society, not only for small conveniences but also for safety-critical tasks. To cope with the ever-increasing complexity of software systems, tools and techniques are needed that support software developers to fully comprehend the behaviours of the systems they develop. In order for such tools and techniques to be truly impactful in real-world scenarios, it is important that they are applicable during the software development process, by the software developers themselves.

In this talk I will present a model-based program verification approach that allows specifying the intended behaviour of a program as an abstract model, for example during the software design phase. This gives an opportunity to find and fix bugs in the software design, or to prove their absence, at an early stage. The key contribution of the approach is its ability to prove in the implementation phase that the concrete code implementation correctly refines the abstract model, by means of code annotation. We applied our approach on a real-world safety-critical industrial case study, and demonstrate that it can indeed help to detect undesired behaviours within reasonable time, that would otherwise be difficult to find.

---

Previous: Vladimir Zamdzhiev | Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory
Next: Artem Khyzha | Speculative Taint Tracking (and a formal analysis of its protection for speculatively-accessed data)