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

Master in Informatics Engineering — Mestrado em Engenharia Informática

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. Formal modeling 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 Structural modeling with Alloy: signature and field declaration. Instance formalization. Formalizing domain models in first-order logic with Alloy.
5 21 Oct MAC Structural modeling with Alloy: structural constraints, first-order and relational logic.
6 28 Oct MAC Advanced Alloy topics: predicates & functions, higher arity relations, modules, type system. Automatic model-based testing.
  3 Nov   Submission of 2nd assessment exercise.
7 4 Nov MAC Behavioral modeling with Alloy: modeling and validation of state transition systems using temporal logic. Software concept design with Alloy.
8 11 Nov MAC Behavioral modeling with Alloy: specification and verification of requirements in temporal logic. Stuttering. App design with Alloy.
  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.
      TEST
      EXAM

Assessment Exercises

# Tópico Deadline
1 Modeling in PL. 12 Oct
2 Structural modeling with Alloy. 3 Nov
3 Behavioral modeling with Alloy. 17 Nov
4 Development and verification of stateful systems with Why3. 22 Dec

Material

Lecture Slides

Lecture Examples

Exercises

Tests

Bibliography

Tools

Past Editions