Formal Methods in Software Development

<p>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.</p> <p>On the model checking side, we cover the following topics:</p> <p style="margin-left:40px">- a specification language for concurrent processes,<br /> - verifying assertions,<br /> - synchronization,<br /> - verifying safety and liveness properties in temporal logic.</p> <p>On the deductive verification side, we cover the following topics:</p> <p style="margin-left:40px">- 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.</p>