Formal Methods in Software Development
The aim of this course is to teach knowledge and skills in, and judgement about, two important styles of formal methods for reasoning about software: model checking and deductive verification.
Each style will be introduced in three ways: conceptual, theoretical, and practical, using a particular tool. The course builds on skills in firstorder logic and temporal logic, and shows how these formalisms can be applied, and extended, for the verification of software.
On the model checking side, we cover the following topics:
- a specification language for concurrent processes,
- verifying assertions,
- verifying safety and liveness properties in temporal logic.
On the deductive verification side, we cover the following topics:
- a unit level specification language for Java programs,
- a logic for verification of Java programs,
- verification of Java programs, in the sense that the implementation of a unit fulfils the specification.