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,<br> \- verifying assertions,<br> \- synchronization,<br> \- 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,<br> \- a logic for verification of Java programs,<br> \- verification of Java programs, in the sense that the implementation of a unit fulfils the specification.