- cbc - CLIPLab

Lecture next week (March 26th) + cars model (exercise for you)
by Manuel Carro 20 Mar '25

20 Mar '25

Hi, all. As agreed yesterday during the lecture, next week's lecture will take place remotely via zoom at the following (password-protected) URL: https://zoom.us/j/4911012202 Pwd: @cbc The time will be the usual one (3pm to 6pm). The URL & pwd will be active from 2:30pm, in case you want to check your connection ahead of time. I uploaded the slides and model of the course section we finished yesterday. The model includes the deadlock freedom theorem for machine m2, but *without the proof*, which needs manual intervention. I am leaving the discharging of the proof as an exercise for you. I have left hints on how to proceed (at least, one way that worked for me) in the comments in the model. If you take the right steps, it can be done in under five minutes. Remember also that the "Proving" section of the course website (https://wp.software.imdea.org/cbc/proving-tips/) has some general tips that are applicable to this case also. Note: we tend to use p0 to work with the active hypotheses. ml is also good with arithmetic, so it may help as well. Best, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

Lecture on Wednesday, March 26th
by Manuel Carro 17 Mar '25

17 Mar '25

Dear all, I will be out of Madrid on Wednesday, March 26th. In order not to miss the lecture on that day, I suggest to do that session online. The material I expect to cover does not need using Rodin as we were doing during the last sessions, and which can be difficult to do having a VC software open at the same time. We can comment on that this Wednesday. Best, -- Manuel Carro : manuel.carro(a){upm.es,imdea.org} Associate Professor, School of CS, UPM : http://www.fi.upm.es Director, IMDEA Software Institute : https://software.imdea.org Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

Second CbC homework
by Manuel Carro 07 Mar '25

07 Mar '25

The second CbC homework is available. Please check https://wp.software.imdea.org/cbc/2025/03/06/second-event-b-homework-3/ Deadline: Tuesday, March 25th, 23:59. Best, -- Manuel Carro : manuel.carro(a){upm.es,imdea.org} Associate Professor, School of CS, UPM : http://www.fi.upm.es Director, IMDEA Software Institute : https://software.imdea.org Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

List test
by Manuel Carro 26 Feb '25

26 Feb '25

Hi. Sorry about this unexpected message. I have been reviewing the list settings and I am not completely sure messages are going through now. I would be most grateful if one of you replies _to the list_ (so that everyone else can see it and we don't get 30+ different replies) if you receive this message. Thanks, -- Manuel Carro : manuel.carro(a){upm.es,imdea.org} Associate Professor, School of CS, UPM : http://www.fi.upm.es Director, IMDEA Software Institute : https://software.imdea.org Madrid, Spain : +34-91-101-2202 ext. 4140

2 1

Question on termination in problem sheet #1
by Manuel Carro 20 Feb '25

20 Feb '25

Hi. Item 5 of question #2 of the first problem sheet requires to prove termination of the computation of a model. Since in yesterday's lecture we did not reach the point where we deal with proof obligations for termination, you can disregard that item and not answer it. It won't be necessary towards obtaining the maximum grade in this homework. Best, -- Manuel Carro : manuel.carro(a){upm.es,imdea.org} Associate Professor, School of CS, UPM : http://www.fi.upm.es Director, IMDEA Software Institute : https://software.imdea.org Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

First CbC exercise sheet
by Manuel Carro 16 Feb '25

16 Feb '25

Hi, all. The first exercise sheet for Event-B is available at the course website. Please see the announcement at https://wp.software.imdea.org/cbc/2025/02/13/first-cbc-homework-deadline-tu… Best, -- Manuel Carro : manuel.carro(a){upm.es,imdea.org} Associate Professor, School of CS, UPM : http://www.fi.upm.es Director, IMDEA Software Institute : https://software.imdea.org Madrid, Spain : +34-91-101-2202 ext. 4140

1 1

Installing Rodin (Event-B development environment)
by Manuel Carro 13 Feb '25

13 Feb '25

It is very likely that we can start using Rodin next week (Wednesday, Feb. 19th). To get the most of the lectures, please install Rodin in your laptops and bring them to the classroom so that we can start to develop models and prove properties. Please have a look at https://wp.software.imdea.org/cbc/rodin-installation-and-tips/ for instruction installations and some generic advice! Best, -- Manuel Carro : manuel.carro(a){upm.es,imdea.org} Associate Professor, School of CS, UPM : http://www.fi.upm.es Director, IMDEA Software Institute : https://software.imdea.org Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

Welcome to the Correctness by Construction course
by Manuel Carro 27 Jan '25

27 Jan '25

Hi! If you receive this email, you have registered for the Correctness by Construction course. This course is taught in three different master programs: MFII, EMSE, and MUSS. In addition, it is part of the eligible requirements for the DSSC PhD program. The mailing list and the web page will be our primary communication means outside the classroom. The web page is located at https://wp.software.imdea.org/cbc/ Please read it thoroughly and let me know if there is something unclear (or just wrong). You can send messages to the mailing list using the address cbc(a)software.imdea.org Messages to the mailing list will reach *all* of your classmates. You are free to use it, but only for messages that can be read by everyone. This mailing list uses the official mail addresses provided by the university where you registered. Please make sure you read it frequently. Please also let your classmates who are registered in this course know that this message has been sent. The lectures will take place in the Montegancedo Campus of UPM on Wednesdays from 3pm to 6pm at classroom 6205 (building 6, level 2, room 05). The first lecture will take place on *February 5th*. -- Manuel Carro : manuel.carro(a){upm.es,imdea.org} Associate Professor, School of CS, UPM : http://www.fi.upm.es Director, IMDEA Software Institute : https://software.imdea.org Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

Tercer intento
by Manuel Carro 27 Jan '25

27 Jan '25

1 0

A test, again
by Manuel Carro 27 Jan '25

27 Jan '25

Let us see if this goes through

1 0

2026

2025

2024

2023

2022

2021

2020

cbc