Formal Methods in Software Development

Education facts

Code: DIT272

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.

Entry 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.

Education offerings

Each offering has its own dates and conditions. Closed offerings are retained as history and do not mean that a new application is open.

• Formal Methods in Software Development

  University of Gothenburg

  Start date: 1 September 2025

  End date: 2 November 2025

  Pace of study: 50 %