Jump directly to:
Lecturers and office ours
Logic and computer science
The RODIN Tool
Floyd-Hoare / Dafny
Schedule (subject to change)
- 13/09/2017: General introduction.
- 18/10/2017: Introduction to Event-B witht the slides up-to-date
- 25/10/2017: No lecture (attending conference)
- 31/10/2017: Lecture corresponding to Thursday 1/11/2017
(holidays) and up-to-date slides covering: event
example, simple invariants, invariant establisment
- 2/11/2017: Sequent calculus, deduction rules, invariant
proofs, (non-)inductive invariant, termination, postconditions.
Up-to-date Slides. Very
recommended reading: sections 3.3, 6.4, and 6.5 of Logic and
Proof (Lawrence Paulson's course notes). A very good book to
in Computer Science: Modelling and Reasoning about Systems.
- 8/11/2017 Slides on Refinement (first
part). Searching in a sorted array. Constants, invariants. Proofs
for refinement. A Model which
performs a random search and refinement which performs a random
search in a narrowing window. This model contains only the proofs
that RODIN performs automatically.
- 15/11/2017 Second session on Refinement
Searching in a sorted array narrowing the search window.
- 22/11/2017 Correction of the exercises. Presentation
of the Cars and bridge example.
- 27/11/2017 Second Event B
homework and the
on which it is based. Deadline: December 20th 2017, 7 pm.
- 13/12/2017 The project term has been posted. Deadline: Sun Jan 14, 2018,
23:59. Presentations: Wed Jan 17, 2018, 7pm to 9pm.
- 20/12/2017 Concurrent system development: access control
for a cashier line: slides, the listing of a model and a RODIN model.
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.
- > 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.
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
- 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 at SourceForge.
- The handbook for
Rodin is also online. It does not correspond the latest tool
version: some details differ, but the basic ideas remain.
- Installation instructions for RODIN.
- The Atelier B Provers plugin is necessary for any
non-trivial development. Install it 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 course examples will not work.
- Interesting sections of the manual (Read them and have them
in you bookmarks):
- How to set
up a Rodin project (but we will see it in the lectures).
- Hints on discharging proofs using RODIN. Do read it. It has many
hints and information on how to use the built-in and external
- An explanation of the proving perspective from the user interface point of
- A catalog of the proof
obligations generated by RODIN and their meaning.
- A list of the rewriting rules
in the default Event B prover (extracted from the Event B
- 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.