Rigorous Software Development

European Master in Software Engineering
Master on Software and Systems


Jump directly to: Overview | Lecturers and office ours | Mailing lists | General papers | Logic and computer science | Event B | Floyd-Hoare / Dafny | Maude | Property-based testing

Schedule (subject to change)

Overview

Software is getting more and more complex and is becoming responsible for critical tasks. Therefore, any technology aimed at ensuring the reliability and quality of software will be increasingly relevant.

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

In this course we will give a hands-on overview of several rigorous software development methods, including both those which follow a "correctness by construction" approach and those which gear more towards verifying software written separately.

Therefore, some goals of the course are:

Knowledge of formal (first-order) logic, proof techniques, functional and logic programming is assumed as a prerequisite.

Lecturers and Office Hours

Mailing lists

The mailing list of the course is at https://babel.ls.fi.upm.es/cgi-bin/mailman/listinfo/rsd-forum. Please subscribe to it using a mail address that you read often. All classroom announcements will go through this mailing list.

Material and resources

Besides the material for every session (in the schedule) we list here additional material of interest to which we may refer in the slides or during the lectures.

General papers and misc. information

Logic and computer science

There are many very good references, but we recommend these two:

Event B

A wealth of information about Event B and associated tools can be found in its website.

The RODIN tool

Rodin is a Eclipse-based tool to develop Event B projects. It includes an editor for all the components of an Event B project, which keeps track of the proof obligations and tries to discharge them. It has a lot of plugins (installable directly from Rodin) which provides advanced theorem proving capabilities (to make it possible to automatically discharge more proof obligations), model-checking, animation, code generation, printout generation, and much more. It is a very good tool and you should install it, as we will use it during the course.

Floyd-Hoare / Dafny

Maude

Property-based testing