Formal Methods in Software Development
About
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,
- synchronization,
- 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.
Prerequisites and selection
Requirements
Successfully completed courses corresponding to 120 credits within the subject Computer Science or equivalent, specifically DIT201 Logic in Computer Science, 7.5 credits, and a 7.5 credits course in object-oriented programming (or equivalent) are required. Applicants must prove their knowledge of English: English 6/English B from Swedish Upper Secondary School or the equivalent level of an internationally recognized test, for example TOEFL, IELTS.
Selection
Selection is based upon the number of credits from previous university studies, maximum 165 credits.
