- cbc - software.imdea.org

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

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

2026

2025

2024

2023

2022

2021

2020

cbc