- cbc - CLIPLab

Lecture for Wednesday 18th: material
by Manuel Carro 15 Feb '26

15 Feb '26

Dear all, next Wednesday, Feb. 18th, I expect to start using Rodin. 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 01 Feb '26

01 Feb '26

Hi. If you receive this email, you have registered for the Correctness by Construction course. It is taught in three different master programs (MFII, EMSE, and MUSS) and it is part of 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, to make sure that everyone is enrolled in the mailing list. 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 4th*. 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

Exams in June and July
by Manuel Carro 08 Jun '25

08 Jun '25

Dear all, I've been asked a couple of times about the course exams. In general, for those who don't pass a course based on homework / partial exams (for these courses where this is a possibility), there is one exam at the end of every semester (i.e., January or June, depending on the semester in which the course takes place) and, additionally, an extra opportunity in July. Those who did not pass because of academic fraud only can go to the July resit. For CbC, this year's dates are: - Wednesday July 11, 3pm-6pm. - Friday July 4, 3pm-6pm. In general the exams take place in the same room as the lectures. If there is any change, I will notify you. As for the format, it is typically the statement of a problem to solve with Event-B and Rodin. It may be a new problem or a variation of previous examples. Plus, all typical programming examples can be replicated: - Insert in a sorted linked list. - Removal of an element in a sorted linked list. - Determine the maximum / minimum of a function (without using the max / min builtin functions). - ... I am attaching a file with suggested exercises you may want to tackle on your own to sharpen your skills. 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 2

Scheduling for the presentation sessions of the term project
by Manuel Carro 16 May '25

16 May '25

Dear all, please find below the proposed schedule for the presentation sessions of the next two weeks. These have been publicly available for several daya, but please let me know if you have any issue. Please try for the presentations to be ~20 min, including questions (but you do not need to use up the whole slot, of course.) There will be 5 min. between presentations to change laptops, etc. Please bring with you a PDF version of your presentation to be able to use another laptop in case of technical problem with yours. The projector has an HDMI input, so if your laptop only has an USB-C (or any other, e.g., DisplayPort?) video output, please try to bring an adapter you know works for you. I always have a USB-C-to-HDMI adapter with me just in case. Lastly, please remember that I expect your models + slides by the day before, Tuesday May 20th, 23:59. Wednesday, May 21st. ==================== 15:10-15:30 The Rodin Stones 15:35-15:55 Event-NEA ----------- break -------------- 15:05-16:15 Thinking 16:20-16:40 Andachris ----------- break -------------- 16:50-17:10 SchRodingers 17:15-17:35 Álvaro Sanz Wednesday, May 28st. ==================== 15:10-15:30 Los primos 15:35-15:55 Plan B ----------- break -------------- 15:05-16:15 Forca Barca 16:20-16:40 PDD ----------- break -------------- 16:50-17:10 Rodinhood 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

Software for today's (Wed May 7) lecture
by Manuel Carro 07 May '25

07 May '25

Hi, all. During today's lecture I intend to use an additional Rodin plugin. It would be great if you install it ahead of time. If you cannot, we'll do it during the lecture. It's the ProB model checker. Please install it by selecting the menu entry Help -> Install new Software . In the "work with" input box type "prob" and a url will appear. Select it, and the select the "ProB for Rodin" plugin that should appear listed below (if you expand the plugin, four components should show up; select all of them). Click "Next" at the bottom of the window, wait, restart and you should be good to go. You may want to install as well the SMT solvers package: - Go to "Install new software". - In the "Work with" input, click on the right downwards arrow to open a pull-down menu, select "All available sites". - In the list, scroll down to locate "Prover extensions". - Expand "Prover extensions" clicking on the ">" sign on the right. - Select "SMT Solvers" - Click "Next", wait for it to install, restart. - You will then have a new "SMT" button in the Theorem Prover perspective. 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

Extension of submission for homework #3
by Manuel Carro Liñares 30 Apr '25

30 Apr '25

Dear all, Given yesterday's power outage, which has surely disrupted many of your regular workflows, the submission of the third homework is extended for 24 hours - until tomorrow Wednesday, April 30th, at 23:59. Best regards, Manuel ⁣Sent from mobile. Please excuse brevity. Get TypeApp for Android

2 1

Term project
by Manuel Carro 13 Apr '25

13 Apr '25

The term project is available at https://wp.software.imdea.org/cbc/2025/04/12/term-project-3/ Deadline to send the material: Tuesday, May 20th, 23:59. Best regards, and have a good Easter! -- +-----------------------------------------------------------------------------+ | 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

Planning term project presentation --> Provide info by Monday 14th, EOB
by Manuel Carro 09 Apr '25

09 Apr '25

Hello everyone. As I mentioned today during the lecture, we have to plan the presentation of the term project . I usually require groups of *three people* to work jointly on the project and make a presentation. According to the last homework submissions, I assume there will be around 10-11 groups. Squeezing the presentations in a single 3-hour session is possible, but it'll be way too tight. The date for the regular / final exam is June 11th @ 3pm (and it can be retaken on July 4th). Whoever passes the course with homework + term project does not need to go to the final exam. But everyone has the right to take that exam instead of the homework; and there may be people who do not pass with homework + project, and prefer to take the June exam instead of the July exam. So, June 11th has to be saved for this possibility. The last lecture day is Wed, May 28th. So my proposal is use Wed, May 21st and Wed, May 28th, to make the presentations. Therefore, I am asking you to please provide information regarding your availability on May 21st and 28th, as well as data for the groups for the term project. Please go to the Google Docs spreadsheet at https://docs.google.com/spreadsheets/d/1BTdeDeLeFBbUbxxj-6xEdQY5odPkPS6IROe… and: 1.- Fill in your name. 2.- State whether you could make a presentation on May Wed 21st. If you can do it in both dates, please mark both (this should probably be the default, as both days are regular lecturing days), and whether you can stay for the presentation one hour more (until 7pm), just to know which possibilities we have. 3.- When you know who is going to be in the group with you, give the group a name and associate the members of the group with that name. You can name your group "Group N" for some number, but some imagination won't hurt 😁. Please provide the information as early as it is possible for you, and in any case before next Monday, April 14th, EOB. 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

Third Event B Homework (2025)
by Manuel Carro 31 Mar '25

31 Mar '25

Dear all, the third Event B homework is ready. Please access it at https://wp.software.imdea.org/cbc/2025/03/31/third-event-b-homework-2/ Note that the PDF linked there contains internally a link to a Rodin model for the "Phone Agenda" refinement task. You should download and refine it. Deadline to turn in the models: April 29th, 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

Rodin installation on Mac
by Leon Schlößer 24 Mar '25

24 Mar '25

Hello, I am currently having issues while trying to install Rodin on my new Macbook. I always get the same error similar to "Library/Java/JavaVirtualMachines/temurin-17.jdk/Contents/Home/bin/.../lib/server/libjvm.dylib" does not contain the JNI_CreateJavaVM symbol". Has anyone of you encountered a similar problem and might be able to help me with installing? Best regards Leon Schlößer

1 0

2026

2025

2024

2023

2022

2021

2020

cbc