- cbc - software.imdea.org

Masks in lectures
by Manuel Carro 19 Apr '22

19 Apr '22

Dear all, as you may know, starting tomorrow, Wednesday 19th, the regulations regarding mask usage in Spain will be relaxed: they will not be mandatory in closed spaces (with a few exceptions). However, institutions and companies are free to require their use. UPM has decided to continue requiring the use of masks in its premises. So, please bring masks tomorrow to the lecture. 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

Correctness by Construction: HW #3
by Manuel Carro 19 Apr '22

19 Apr '22

Hi. The third homework for Correctness by Construction is available at https://wp.software.imdea.org/cbc/2022/04/19/third-cbc-homework/ . The deadline to turn it in is May 4th, 2022. Best regards, -- +-----------------------------------------------------------------------------+ | 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 by zoom on Wednesday, April 6th
by Manuel Carro 05 Apr '22

05 Apr '22

Dear all, apparently a dysfunction in the heating system of the CS school, combined with the low temperatures in Madrid now, has forced the School to stop face-to-face lectures for the rest of the week. We have been asked to use Zoom / MS Teams instead. Therefore, tomorrow's lecture will be delivered via Zoom at the normal slot (4pm to 7pm). The coordinates are below: URL: https://zoom.us/j/5911012202 Password: CorByC Sorry about this late announcement -- I have just become aware of it. Best regards, -- +-----------------------------------------------------------------------------+ | 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

Section 3.3 of HW #2 + extension
by Manuel Carro 01 Apr '22

01 Apr '22

Hi. I have received several questions regarding section 3.3 of HW2. Some of you have reasoned along the lines of "when the event Finish is enabled, then f(r) = y and we have found what we wanted". That is true, but it is not an answer. First of all, Finish might never be enabled; we never proved explicitly it was going to be enabled. Second, and more important: Finish is an artifact that appears in the model only to highlight a condition in which a sequential algorithm would have exited from a loop. But it does not do anything, and we may as well remove it and nothing changes in the model: all the proofs we discharged can still be discharged. So, let us assume that Finish does not exist and things will be clearer. Section 3.3 asks: how would you prove that IF the model eventually stops, then we will have found the location of 'v'? And I am asking you to find out a logic formula such that if it can be inferred from the axioms and the invariants, then the model eventually finds the location of 'v'. And, furthermore, you should be able to introduce this formula in Rodin as an invariant (perhaps marked as 'theorem') and, if Rodin discharges the formula, then you would have proved that the model eventually finds an r s.t. f(r) = v. Since this clarification is coming somewhat late, I will be accepting homework until Monday, April 4th, 23:59 without any penalty. Greetings, -- +-----------------------------------------------------------------------------+ | 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

Correctness by Construction: second homework
by Manuel Carro 21 Mar '22

21 Mar '22

Hi, all. The second homework for the Correctness by Construction course is available. Please access it at https://wp.software.imdea.org/cbc/2022/03/20/second-cbc-homework/ Deadline to turn it in: Saturday, April 2nd, 00:01. Send it to me by email. I recommend to have a look at it before next lecture so that I can answer any question with time enough. Best regards, -- +-----------------------------------------------------------------------------+ | 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 1

Virtual machine with Rodin
by Manuel Carro 07 Mar '22

07 Mar '22

I have been asked by some of you whether I can provide a virtual machine with Rodin installed, because in someone's installation icons do not appear (as in mine). First of all, icon placement may differ among instances because you can change the interface and move things around, and also depending on the plugins one has installed, more / less icons will appear. So I would anyway ask you to double check the informacion at https://wp.software.imdea.org/cbc/proving-tips/ https://wp.software.imdea.org/cbc/rodin-installation-and-tips/ https://www3.hhu.de/stups/handbook/rodin/current/html/proving_perspective.h… and try to identify / locate the icons and menus referred there. I have notwithstanding left at https://wp.software.imdea.org/cbc/rodin-installation-and-tips/ under "If everything fails" a pointer to an Ubuntu virtual machine with minimal instructions. Use it only if necessary. A native installation will be better because you do not have to worry about assigning threads, memory, disk to the virtual machine. 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 Wed. 2 --> remote
by Manuel Carro 02 Mar '22

02 Mar '22

Dear all, an unexpected personal matter has forced me to leave Madrid, so I will not be able to be physically present for today's (Wednesday's) lecture. Since the time available for lectures is limited, instead of cancelling the lecture I am suggesting to exceptionally do it online: everyone will connect to a zoom session and this lecture will take place via zoom. If this is an issue for anyone, please let me know so that we can try to work out an alternative solution. In parallel, I am checking with University officials that I am not breaking any regulation. Therefore, and if nothing forbids it, we will meet on Wed. 2 at 4pm-ish on https://zoom.us/j/5911012202 Pwd: @CbC Sorry again for this sudden change! Best regards, -- +-----------------------------------------------------------------------------+ | 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

First Event-B exercise sheet
by Manuel Carro 22 Feb '22

22 Feb '22

Hi, all. The first exercise sheet for Event-B is available at the course website (please access it through https://wp.software.imdea.org/cbc/2022/02/22/first-cbc-homework/). 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

For today's lecture: bring laptops if you can!
by Manuel Carro 16 Feb '22

16 Feb '22

Hi, everyone. I should have sent this mail before -- sorry! If you can, bring your laptop to the lecture today and have Rodin installed, as explained at https://wp.software.imdea.org/cbc/rodin-installation-and-tips/ Time permitting, we will type some models together. If you cannot install Rodin / bring a laptop, it is completely OK. I will be constructing models live, but typing along with me instead of just watching provides a better experience, as you can make questions and learn from your mistakes. Last, if you bring a laptop, please make sure its batteries are full. I've realized that there are not many plugs in the lecture room, and they are placed inconveniently. I will try to amend this, but I am afraid it won't be possible for today's lecture. 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

Attending lectures remotely
by Manuel Carro 02 Feb '22

02 Feb '22

The slides for today's lecture have been posted at https://wp.software.imdea.org/cbc/ Besides, some of you were attending today's lecture remotely. The CS School sent information on how to deal with that situation. For those who did not receive / did not read the emails sent by the CS School, if you want to attend any lecture remotely you *have to* request it by filling in the form at https://forms.office.com/r/rt45PD9SEM (there is an English version; please select it at the top right corner). The School management will forward me the names of those who can attend remotely. By UPM policy, these are the only students to whom we are allowed to accept in remote lectures. Cheers, -- +-----------------------------------------------------------------------------+ | 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

2026

2025

2024

2023

2022

2021

2020

cbc