Jump directly to:
Lecturers and office ours
Logic and computer science
Floyd-Hoare / Dafny
Schedule (subject to change)
- 13/09: General introduction.
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
Therefore, some goals of the course are:
- To motivate the use of technologies in software
development under the correctness-by-construction
- To study different families of languages and
technologies aimed at easing the process of building
- To understand the differences between declarative and
procedural languages and the impact of these aspects in
- To identify the better niches for the industrial
application of declarative / correctness by construction
Knowledge of formal (first-order) logic, proof techniques,
functional and logic programming is assumed as a prerequisite.
- Manuel Carro office 036 at the IMDEA Software
Institute and D-3323 (under appointment) - mcarro |at| fi DOT upm
DOT es Office hours: send me a mail to get an
- Julio Mariño D-2310 - jmarino |at| fi DOT upm
DOT es Office hours: send me a mail to get an
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
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.
There are many very good references, but we recommend these two:
- Lawrence Paulson's Logic and
Proof notes and slides. Very good introduction to a series of topics related
with logic. We advise reading at least the part related to
propositional logic and first order logic, including proof systems.
- Michael Huth and Mark Dermot Ryan's Logic
in Computer Science: Modelling and Reasoning about Systems,
available in printed form at the Schools library. This is a truly
delightful book that we personally recommend reading back to back.
It relates logic with many areas of Computer Science with clear
examples and is likely to open your perception of what logic and
Computer Science have in common.
Mathematical Logic for Computer Science. Mordechai
Ben-Ari. Springer, 2001. There should be copies in the School's
A wealth of information about Event B and associated tools can
be found in its website
- The most comprehensive reference about Event B is the book Modeling in Event-B: System
and Software Engineering, published
by Cambridge University Press. There is an errata sheet. The
School has at least one copy. Parts of the book, as well as
supporting material, are freely available at the Event B website.
All the slides corresponding to the book chapters are available
online. They are not a substitute for the book but they are
almost self-explanatory. Rodin project files for the projects in
every chapter are also available.
- A summary of the Event
- A reference
card with the deduction rules, the structure of Event
B models and events, the formal definition of the proof
obligations, and the ASCII syntax to write the symbols in
- Slides presenting
rules, overview of first-order predicate calculus, set
theory, and relations.
- An introduction to the Event-B method with a description of
- A paper about refinement and
decomposition in Event B. It is probably too abstract and
advanced for the aims of this course, but the first five sections
can probably be understood without too many problems.
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
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.
- Homepage of
version of the Rodin Event B development method. Please ensure
that this is actually the latest version by checking
the Core Rodin homepage.
- Please find here installation instructions.
- Of all the plugins, the most interesting for us is the
Atelier B Provers. Install them by going to
Help ⇒ Install new software ⇒ select
Atelier B Provers ⇒ Select in box ⇒ Click
Next ⇒ Follow instructions. If you do not install
these provers, most of the examples in the course will not work out
of the box!
- The handbook for
Rodin is also online.
- All of
rules in the default Event B prover (this is extracted
from the Event B website).
- Exercise sheet on algebraic specification using Maude.
- Algebraic Specification. Martin Wirsing. A chapter in the
Handbook of Theoretical Computer Science, Vol. B: Formal
Models and Semantics. Elsevier, 1990. ISBN 0 444 88074 7.
About Maude -- A High Performance Logical Framework. Clavel,
M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J.,
Talcott, C. Lecture Notes in Computer Science, vol. 4350.
- An introduction to
- A manual for Maude.
- The source code used in my QuickCheck demo (Haskell).
- A short essay explaining how to use Erlang QuickCheck for
testing Java programs.