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

Schedule and material

• General introduction and motivation. Software development from a practitioner's point of view. The meaning of the "rigorous" tag. How relevant/serious/lethal can software bugs be? When is it worth to invest in guaranteeing that a piece of software is certified to have no errors at all? Critical software, software horror stories, cyber physical systems. You can have a look at this (rather outdated) collection of horror stories or you may rather think about examples around you (e.g. the recent Boeing 737 max 8 crashes, etc.)
• Course overview: Formal methods and different ways of doing rigorous SW development. A closer look at how software bugs happen, and provided some examples of programs which, yet small in size (lines of code) may exhibit a complex behaviour. "While programs". Limitations of testing and the need for a formal notation for specification. A more realistic example (sorting). The need for the use of first-order logic as part of any useful specification formalism for software. Course overview, different approaches to rigorous SW development.
  • Slides: course overview.
  • Code: euclid, mystery and hotpo
  • More information on the Collatz conjecture here.
• Floyd-Hoare logic: an introduction. Floyd-Hoare logic is the foundation for most of the formal verification techniques. The basic notions (Hoare triples, while programs, program states) are introduced and the simplest deduction rules.
  • Slides: spoiler-free version of the slides.
  • "Assigning Meanings to Programs" by Robert Floyd is a very accessible presentation of the ideas later formalised by Hoare.
• Floyd-Hoare logic and Dafny. The "tricky" rules of Floyd-Hoare logic: assignment and loops. The concept of weakest precondition and the role of loop invariants for the whole verification process. The Dafny tool for certified programming.
  • Take a tour of the Dafny tool by running and hacking simple quizzes here.
  • Take the Dafny tutorial.
  • Optionally, you can also have a look at Paqui Lucio's tutorial.
• Wrapping up Floyd-Hoare and Dafny.
  • Full version of the Floyd-Hoare slides.
  • Exercise sheet on program verification (Hoare logic and Dafny).
• Executable specifications I.
• Executable specifications II.
Exercise sheets for executable specifications:
• The exercise sheet on Maude.
• The exercise sheet on Prolog.
Solve exercises 1 to 6. For a given exercise i you may choose it from either sheet.
• Introduction to Event-B. Industrial systems requiring total correctness. Usual approaches. Event B basics: refinement, transitions systems, events. First steps: search in an array. Specification of division. Code and events. Invariants. Invariant establishment. Invariant preservation. Sequents. Inference rules. Basic inference rules and axioms. Invariant proofs. More inference rules: disjunctions, conjunctions. More invariant proofs. Inductive and non-inductive invariants. Strength. Proof by contradiction. Sequential correctness. Termination. Slides.
• Introduction to Rodin. Using Rodin for a simple project (live). Refinement example: sequential search in a sorted array. Specification. First model (with Rodin). Refinement idea. Event B model and intuition behind correctness. Sequential search in a sorted array. Refinement by shrinking the selection windows. New proofs associated to refinement: When is a refinement correct? A non-trivial invariant proof, step by step. Using Rodin for (almost) automatically discharge proofs. Slides.

  Rodin models used in the lecture (please follow the instructions in the slides to load them):

  • The integer division example. I really recommend you to try to do at least this one it on your own.
  • The first model of the binary search example.
  • The second (refined) model of the binary search example.
  Try to reproduce them on your own.
• First Event-B Exercise Sheet. Please refer to the homework text for more details on how to turn it in.
• Second Event B exercise. In this exercise, you are asked to use Rodin to make a refinement of a model (download here) thoroughly explained in a previous lecture. If done correctly, it takes approximately three minutes, total! But, of course, it takes some trial and error the first time.
• The Coffee Club. Abstract model and two refinements with proofs (Rodin sources). A difficult requirement: everyone has right to his/her possessions. Limitations of default mathematical toolkit. Possibility of theory extensions.
• Event B term project.
• Sequential vs. concurrent and reactive models. Checkout lines in a market. System and environment events and variables; isolation. Assumptions on the behavior of environment. Identification of the variables, events. Physical interpretation of values of variables. Invariants. Slides and Event B model.

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:

• To motivate the use of technologies in software development under the correctness-by-construction paradigm.
• To study different families of languages and technologies aimed at easing the process of building correct software.
• To understand the differences between declarative and procedural languages and the impact of these aspects in software development.
• To identify the better niches for the industrial application of declarative / correctness by construction technologies.

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

Lecturers and Office Hours

• 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 set up an appointment.
  
• Julio Mariño
  D-2310 - jmarino |at| fi DOT upm DOT es
  Office hours: send me a mail to set up an appointment.

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

• A collection of Software horror stories. The video of the Ariane 5 incident is a well known case.
• Some examples of the use of formal methods in industry.
• The challenge of producing verified software and some advances. The project goes on.
• A survey on the current applications of formal methods in industrial settings.
• A brief account of several formal specification methods and the road ahead.
• J. R. Abrial's Faultless Systems: Yes, we Can. A rationale for modern rigorous development methods by the creator of Event B.
• A survey on loop invariants. Section 3.2 has tips on how to find out invariants and Section 4 includes examples of invariants for many common algorithms. Note: it only deals with sequential systems.

Logic and computer science

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 School's 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 library.

Event B

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 B language.
• 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 Event B.
• Slides presenting the inference rules, overview of first-order predicate calculus, set theory, and relations.
• An introduction to the Event-B method with a description of its phases.
• 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 (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.

• Homepage of the Rodin versions. Please make sure to download the latest version.
• 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 theorem provers.
• An explanation of the proving perspective from the user interface point of view.
• 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 website).

Floyd-Hoare / Dafny

• Slides on Floyd-Hoare logic (version without spoilers).
• Exercise sheet on program verification (Hoare logic and Dafny).Y

Maude

• 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.
• All 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. (Free download from a UPM IP address.)
• An introduction to Maude.
• A manual for Maude.

Property-based testing

• The source code used in my QuickCheck demo (Haskell).
• A short essay explaining how to use Erlang QuickCheck for testing Java programs.