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
- Logics for formal specification
- Propositional logic (PL)
- First-order logic (FOL)
- Relational logic (RL)
- Linear temporal logic (LTL)
- Automated proof techniques
- SAT solving for propositional logic
- SMT solving for first-order logic and theories
- Model-finding via SAT for relational logic
- Bounded model-checking via SAT for temporal logic
- Formal software design with Alloy
- Structural modeling
- Behavioral modeling
- Automatic model-based testing
- Program specification and verification with Why3
- Logical language, theories (library), and proof
- Programming language, behavioral specification, and correctness verification
- Development of stateful systems
Teaching Team
- Nuno Macedo (NM)
- Jorge Sousa Pinto (JSP)
- Maria João Frade (MJF)
Assessment
- Continuous Assessment
- Assessment Exercises (20%)
- Individual test (80%)
- Final Exam
- Individual exam (100%)
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. |
| 14 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. | 14 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
- Class 3
- Class 4
- File system with Alloy (and theme)
Exercises (TP classes)
- Propositional Logic Modeling
- Firs-Order Logic Modeling
- SAT solvers & SMT solvers and Colab notebooks:
- Mobile Phone (solved)
- Colocação de Paineis (144 variantes)
- Distribuição de Gabinetes (36 distribuições possíveis)
- Alocação de Aulas (224 alocações possíveis)
- Survey (11 variantes)
- Structural Design with the Alloy Analyzer
Tests
Bibliography
- Logic in Computer Science: Modelling and Reasoning About Systems. Michael Huth & Mark Ryan. Cambridge University Press; 2nd edition (2004).
- The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley & Zohar Manna. Springer (2007).
- Rigorous Software Development: An Introduction to Program Verification. J.B. Almeida & M.J. Frade & J.S. Pinto & S.M. de Sousa. Springer (2011).
- Software Abstractions: Logic, Language, and Analysis (revised edition). Daniel Jackson. MIT Press (2012).
- The Essence of Software: Why Concepts Matter for Great Design. Daniel Jackson. Princeton University Press (2021)
- Formal Software Design with Alloy 6. Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo (2021).
Recommended Reading
- D. Jackson. Alloy: a language and tool for exploring software designs. Commun. ACM 62(9): 66-76 (2019). Também existe um vídeo sobre este artigo que pode ser visto aqui.
- Leslie Lamport. If You’re Not Writing a Program, Don’t Use a Programming Language. Bulletin of the EATCS 125 (2018)
- David Benavides, Sergio Segura, Antonio Ruiz Cortés: Automated analysis of feature models 20 years later: A literature review. Inf. Syst. 35(6): 615-636 (2010)
Tools
- SAT solvers
- SMT solvers (SMT-LIB - The Satisfiability Modulo Theories Library)
- Alloy
- Why3