cbc March 2025

cbc@software.imdea.org

2 participants
5 discussions

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

2026

2025

2024

2023

2022

2021

2020

cbc March 2025