{"id":20,"date":"2020-01-08T17:41:11","date_gmt":"2020-01-08T17:41:11","guid":{"rendered":"https:\/\/wp.software.imdea.org\/cbc\/?page_id=20"},"modified":"2026-03-26T11:55:20","modified_gmt":"2026-03-26T10:55:20","slug":"main-cbc-page","status":"publish","type":"page","link":"https:\/\/wp.software.imdea.org\/cbc\/","title":{"rendered":"A Course on Correctness by Construction"},"content":{"rendered":"\n

Motivation and Goals<\/h1>\n\n\n\n
\n
\n

Software is becoming increasingly complex and responsible for critical tasks. Any technology aimed at ensuring the reliability and quality of software will be increasingly relevant, if not utterly necessary.<\/p>\n\n\n\n

Only rigorous<\/em> (e.g., mathematically sound) approaches can certify software with the highest possible assurance. These approaches include, among others, the use of specification languages, high-level programming languages (including equational, functional, and logic languages), the use of model checking and deductive verification, language-based approaches often interacting with theorem provers.<\/p>\n\n\n\n

In this course we will give a hands-on introduction to rigorous software development methods that follow a “correctness-by-construction” approach. <\/p>\n<\/div>\n\n\n\n

\n

While the course is not heavy in theory, everyone is expected to have a good understanding of first-order logic and programming experience. We will explore several methodologies that have approaches and underlying technical bases, but which share a common overarching goal: develop programs while making sure that non-trivial properties, expressing high-level design requirements regarding correctness, fairness and sometimes efficiency, are continuously respected.<\/p>\n\n\n

\n
\"\"
OR-Left<\/figcaption><\/figure>\n<\/div><\/div>\n<\/div>\n\n\n\n
\n

To follow this course, you should have programming experience (three years or more), familiarity with formal (first-order) logic, formal proofs, logic programming, and concurrent programming. If you think you do not meet these requirements, please get in touch ASAP with one instructor to recommend you reading material.<\/p>\n<\/blockquote>\n\n\n\n

\n

Course Log and Pointers to Class Material<\/h2>\n\n\n\n

Click on the dates to expand the lecture’s content.<\/p>\n\n\n\n

System Modelling using Refinement and Interactive Theorem Proving<\/h3>\n\n\n\n
\n
04\/02\/2025<\/strong>: Intro to rigorous methods and a first taste of Event B<\/summary>
\n

We gave an overview of pitfalls in software development and initial ideas on formal methods<\/a> and we started with a gentle, informal introduction to Event B<\/a>.<\/p>\n<\/div><\/details><\/div>\n\n\n\n

11\/02\/2025: <\/strong>Introduction to Event-B<\/summary>
\n

We continued with Event-B with the definition of a system that captures the behavior of an algorithm to make integer divisions. Slides here<\/a>.<\/p>\n<\/div><\/details><\/div>\n\n\n\n

18\/02\/2025:<\/strong> Inferences in propositional logic, predicate logic, a Rodin example.<\/summary>
\n

We finished our sessions on logic and inference rules<\/a> and we crafted a small example<\/a> in Rodin.<\/p>\n<\/div><\/details><\/div>\n\n\n\n

25\/02\/2025<\/strong>: Developing the model of a sequential program<\/summary>
\n

We started an example of the development of the model<\/a> of a sequential program following these slides<\/a>.<\/p>\n<\/div><\/details><\/div>\n\n\n\n

4\/3\/2025<\/strong>: Refinements and binary search<\/summary>
\n

We continued with the development of the model and correctness proof of a search algorithm – in particular, binary search in a sorted array. Here are the slides<\/a> and the model<\/a> as it was finished in the classroom.<\/p>\n<\/div><\/details><\/div>\n\n\n\n

11\/3\/2025<\/strong>: A reactive, concurrent system: Cars on a Narrow Bridge<\/summary>
\n

We finished the material on sequential development<\/a> with some considerations on theorems and well-definedness for the implication. We started working on reactive systems<\/a> with the first steps of a model<\/a> for software to control cars on a bridge.<\/p>\n<\/div><\/details><\/div>\n\n\n\n

18\/3\/2025<\/strong>: A reactive, concurrent system: Cars on a Narrow Bridge<\/summary>
\n

We continue building the model<\/a> and we are halfway with adding traffic lights<\/a>.<\/p>\n<\/div><\/details><\/div>\n\n\n\n

25\/05\/2025<\/strong>: Comments on the homework; finish the “Cars on a Narrow Bridge” example.<\/summary>
\n

I made some comments on the homework<\/a> and solved the exercises. We finished the example of the cars on the bridge. here are the final slides<\/a> and the model<\/a> as we finished it in the classroom.<\/p>\n<\/div><\/details><\/div>\n\n\n\n

01\/04\/2025<\/strong>: No lecture (Easter Holidays)<\/summary>
\n

<\/p>\n<\/div><\/details><\/div>\n\n\n\n

08\/04\/2025<\/strong>: <\/summary>
\n

<\/p>\n<\/div><\/details><\/div>\n\n\n\n

15\/04\/2025<\/strong>: <\/summary>
\n

<\/p>\n<\/div><\/details><\/div>\n\n\n\n

22\/04\/2025<\/strong>: No lecture. This Wednesday will have the lectures of a Friday at UPM to compensate for other Fridays without lectures.<\/summary>
\n

<\/p>\n<\/div><\/details><\/div>\n\n\n\n

29\/04\/2025<\/strong>: <\/summary>
\n

<\/p>\n<\/div><\/details><\/div>\n\n\n\n

06\/05\/2025<\/strong>: <\/summary>
\n

<\/p>\n<\/div><\/details><\/div>\n\n\n\n

14305\/2025<\/strong>:<\/summary>
\n

<\/p>\n<\/div><\/details><\/div>\n<\/div>\n\n\n\n

Project Presentation Sessions<\/h3>\n\n\n\n

We plan one or two presentation sessions. We may have to use additional sessions depending on the number of project teams. <\/p>\n\n\n\n

\n
20\/5\/2025<\/strong>: First term project presentation session<\/summary>
\n

<\/p>\n<\/div><\/details><\/div>\n\n\n\n

27\/5\/2025<\/strong>: Second term project presentation session<\/summary>
\n

<\/p>\n<\/div><\/details><\/div>\n<\/div>\n<\/div><\/div>\n\n\n\n

\n\n\n\n
\n

Location, Schedule, Administrivia<\/h1>\n\n\n\n

Place and time<\/h2>\n\n\n\n

During the academic year 2025-2026 we will meet physically at classroom 6205 from 3pm to 6pm on Wednesdays. We will post any exception on the course mailing list (see below) and the course log<\/a>.<\/p>\n\n\n\n

Teaching<\/h2>\n\n\n\n

Manuel Carro (coordinator)<\/h3>\n\n\n\n

Office 035 at the IMDEA Software Institute (under appointment)- mcarro |at| fi DOT upm DOT es.<\/p>\n\n\n\n

Communication<\/h2>\n\n\n\n

For security reasons, you cannot subscribe to the mailing list by yourself. You should have been subscribed by some instructor, and you should have received a welcome message with the initial subscription. Note that you can only post to the list from the mail address that has been subscribed. If you want to change it, please let an instructor know. In normal situations, all important classroom announcements will go through the course mailing list<\/strong>, so please be sure to read the subscribed address regularly.<\/p>\n<\/div><\/div>\n\n\n\n

\n\n\n\n
\n

Course Policy<\/h1>\n\n\n\n

To keep this landing page short, the course policy appears in a separate page<\/a>. This does not mean it is less important<\/strong>. Please make sure to read it.<\/p>\n<\/div><\/div>\n\n\n\n

\n\n\n\n
\n

Academic Resources<\/h1>\n\n\n\n

Please have a look as well at the Assorted Resources<\/a>. It contains not-strictly-academic (but interesting) material!<\/p>\n\n\n\n

Some of the resources below are books. The University library may have a copy of them. Otherwise, copies can be available in several online book shops. Last, it may be possible that copies are freely available on the web; I of course cannot know whether they have been posted with permission from the copyright holders.<\/p>\n\n\n\n

Logic <\/h2>\n\n\n\n