Formal Methods in Software Engineering

Master in Informatics Engineering

2026/27

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

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 ED2 0.05 MAC + JSP
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 23 Sep MAC Course presentation. Propositional logic. Modeling allocation problems and feature diagrams in propositional logic.
2 30 Sep MAC First-order logic. Formalizing domain models in first-order logic.
3 7 Oct MAC SAT solving.
  13 Oct   Submission of 1st assessment exercise.
4 14 Oct MAC Domain modeling with Alloy: signature and field declaration, specifying structural requirements in first-order logic, and validation with scenarios.
5 21 Oct MAC Domain modeling with Alloy: specifying structural requirements with relational logic.
6 28 Oct MAC Advanced Alloy topics: predicates & functions, higher arity relations, modules, type system. Data structure design and model-based testing.
  3 Nov   Submission of 2nd assessment exercise.
7 4 Nov MAC Software concept design with Alloy: modeling and validation of state transition systems using temporal logic.
8 11 Nov MAC Software concept design with Alloy: specification and verification of behavioral requirements using temporal logic, concept composition.
  17 Nov   Submission of 3rd assessment exercise.
9 18 Nov JSP Verification of functional programs with Why3.
10 25 Nov JSP Development of stateful modules in Why3. Finite maps, record types, and type invariants.
11 2 Dec JSP Data refinement in WhyML. Specification and verification of software concepts with Why3.
12 9 Dec JSP Extraction of OCaml code from verified WhyML modules. OCaml implementation of software concepts. Imperative implementation.
  22 Dec   Submission of 4th assessment exercise.
  6 Jan   TEST
  27 Jan   EXAM

Assessment Exercises

# Tópico Deadline
1 Modeling with propositional logic. 13 Oct
2 Specification and validation of structural requirements. 3 Nov
3 Specification and verification of behavioral requirements. 17 Nov
4 Development and verification of stateful systems with Why3. 22 Dec

Material

Lecture Slides

Lecture Examples

Exercises

Tests

Bibliography

Tools

Past Editions