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 first-order 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.