Formal Methods in Software Engineering — Métodos Formais em Engenharia de Software

Master in Informatics Engineering — Mestrado em Engenharia Informática

2025/26

This course unit in the first semester of the first year of the Master in Informatics Engineering at the University of Minho aims to introduce the use of Formal Methods in Software Engineering.

Students interested in deepening the knowledge acquired in this course unit may choose to attend the Formal Programming Methods specialization track in the second semester.

Syllabus

Teaching Team

Assessment

The assessment exercises will be proposed at the end of (some) lectures and are to be submitted on the e-learning platform by the following Sunday.

For both continuous and final exam assessment, grades above 18 must be defended through the completion of a small project/challenge.

Timetable

Type Class Time Room Instructor
Lecture / Teórica   Wed/4ª 9h-10h ED1 0.08  
Tutorial / Teórico-prática 1 Wed/4ª 11h-13h ED2 0.01 JSP
Tutorial / Teórico-prática 2 Wed/4ª 11h-13h ED3 0.06 MJF
Tutorial / Teórico-prática 3 Wed/4ª 11h-13h ED1 2.26 NM

Planning

# Date Instructor Summary
1 24 Sep NM Course presentation. Propositional logic. Formal modeling in propositional logic.
2 1 Oct NM First-order logic. Formalizing domain models in first-order logic.
3 8 Oct NM SAT solving.
  12 Oct   Submission of 1st assessment exercise.
4 15 Oct NM Structural modeling with Alloy: signature and field declaration. Instance formalization. Formalizing domain models in first-order logic with Alloy.
5 22 Oct NM Structural modeling with Alloy: structural constraints, first-order and relational logic, predicates and functions.
6 29 Oct NM Advanced topics on structural modeling with Alloy: higher arity relations, overloading, type system. Automatic model-based testing.
  2 Nov   Submission of 2nd assessment exercise.
7 5 Nov NM Behavioral modeling with Alloy: modeling and validation of state transition systems using temporal logic. Software concept design with Alloy.
8 12 Nov NM Behavioral modeling with Alloy: specification and verification of requirements in temporal logic. App design with Alloy.
  16 Nov   Submission of 3rd assessment exercise.
9 19 Nov JSP Program verification of functional programs with Why3.
10 26 Nov JSP Development of stateful modules in Why3. Verification of invariants.
11 3 Dec JSP Specification and verification of software concepts in Why3. Functional implementation.
12 10 Dec JSP Refinement of modules in Why3 and extraction of correct WhyML code. Imperative implementation of software concepts.
13 17 Dec   (TP classes only)
  21 Dec   Submission of 4th assessment exercise.
  7 Jan   TEST
  28 Jan   EXAM

Assessment Exercises

# Tópico Deadline
1 Modeling in PL. 12 Oct
2 Structural modeling with Alloy. 2 Nov
3 Behavioral modeling with Alloy. 16 Nov
4 Desenvolvimento e verificação de sistemas com estado em Why3. 21 Dec

Material

Lecture Slides

Lecture Examples

Exercises (TP classes)

Tests

Bibliography

Tools

Past Editions