Master in Software and Systems

Rigorous Software Development

Lecturer (Coordinator):
Manuel Carro
Julio Mariño


First semester




Software is getting more and more complex and is gradually assuming responsibility for critical tasks. Therefore, any technology aimed at ensuring software reliability and quality will be increasingly important.

There are many ways to approach these goals. The declarative approach relies on languages and logics with a solid mathematical foundation. This includes specification languages (VDM, Z, B, Event-B, OBJ, Alloy...), functional programming languages (Haskell, Erlang, λ-calculi...), and logic programming languages (Prolog, CLP, ASP...).

Learning Goals


  1. Introduction
    1. Overview, motivation and challenges for rigorous software development
    2. Review of background: formal logic, proofs...
  2. Correctness by construction
    1. Event-B: Theory and development methods.
    2. Event-B: the Rodin tool
  3. Verification
    1. Classical program verification
    2. The Dafny tool
    3. The Alloy tool
    4. Property-based testing
  4. Specifications
    1. Algebraic specifications
    2. The Maude algebraic specification language

Recommended Reading



Assessment Method

Depending of the number of students, the final grade will be obtained either from:

Exercises for each unit will have the same relative weight for the overall grade, although individual exercises in a given unit can have different weights.

Tuition Language


Subject-Specific Competences

More information:

This table shows the code, description and proficiency level for each subject-specific competence

Code Competence Proficiency Level
SSC1 Examination of the state of the art to identify research problems related to the design, construction, use and evaluation of complex software-intensive sociotechnical systems S
SSC5 Contribution of solutions to open problems related to software verification and validation applications and methods, techniques and tools A

Learning Outcomes

More information:

This table shows the code, description and proficiency level for each subject learning outcome

Code Learning Outcome Associated competences Proficiency level
RA-AV-1 Familiarity with the idea of design and implementation requirement SSC1,SSC5 C
RA-AV-2 Familiarity with different formal development techniques SSC1,SSC5 K
RA-AV-3 Knowledge of several languages for applying formal development techniques SSC1,SSC5 A
RA-AV-4 Knowledge of techniques for proving code correctness SSC1,SSC5 A
RA-AV-5 Effective use of rigorous software construction techniques SSC1,SSC5 C

Learning Guide

Subject learning guide for Rigorous Software Development