- cbc - IMDEA Software

Lecture this week + slots for term project presentations
by Manuel Carro 15 May '26

15 May '26

Hi. I have just sent you the results of the second homework. Thanks for your patience! As I mentioned during the last lecture, we will not have lecture this Wednesday, May 13th. I assume that extra time to prepare the homework and the term project will be welcome! If you have questions, doubts, etc. regarding any topic of the course, please feel free to contact me so that I can assist via email or through videoconference. If you prefer a physical meeting, please let me know as well to find a slot that is convenient for everyone. Besides, we need to assign the slots for the presentations on May 20th and May 27th. Please find a tentative assignment at https://docs.google.com/spreadsheets/d/1jkEzVOIyDXDT_g8PoGqByXD5X8MNPbwYzk5… Please let me know if any of you have a compelling reason to change 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 1

Searching for a team member
by Gonzalo Martín 07 May '26

07 May '26

Hello, We are still looking for a team member for the project. Please contact me if any of you does not have a team. Regards

1 0

Missing team for the project
by Gonzalo Martín 05 May '26

05 May '26

Hello, I’m looking for a team for the term project, so if anyone needs a member, please contact me. Regards, Gonzalo

1 0

Team for the Term Project
by Carolina Garza Bravo 03 May '26

03 May '26

Good morning, everyone. I'm looking for a group for the Term Project. If anyone is missing a member, please write to me.

1 0

HW#3 & Term Project
by Manuel Carro 20 Apr '26

20 Apr '26

Dear all, the third (and last) homework assignment and the term project are available at: https://wp.software.imdea.org/cbc/2026/04/20/third-homework-assignment/ and https://wp.software.imdea.org/cbc/2026/04/20/term-project-4/ respectively. Best regards, -- 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

No CbC lecture on Wed, April 22nd
by Manuel Carro 20 Apr '26

20 Apr '26

There will be no CbC lecture this Wednesday, April 22nd. Instead, UPM's School of Computer Science and Engineering will follow a Friday schedule to compensate for holidays. We'll meet again on Wednesday, April 29th. Best / Saludos, -- 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

No lecture today (Wed Apr 15th)
by Manuel Carro 15 Apr '26

15 Apr '26

Hi, all. I am afraid that today I have been feeling unwell and it does not seem to improve, so I will not be able to teach our lecture. If you are in close connection with other classmates, please let them know so that they don't make the trip to the campus if it's only for CbC. 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

Roding Proofs and the (R) button
by Manuel Carro 31 Mar '26

31 Mar '26

Hi. I have been asked whether using the blue (R) button is a valid way to discharge proofs. The short answer is no. The blue (R) button does *not* discharge any proof, as it does not try to prove anything. It stands for "Reviewed" and it is a way to tell Rodin "do not bother me with this proof; I am completely sure it's correct" or "I will do that later; I want to continue doing other things now". So, blue bullets in the Proof Obligation panel on the right cannot be accepted as a discharged proof. 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

Second exercise sheet 2026
by Manuel Carro 16 Mar '26

16 Mar '26

Dear all, the second exercise sheet for the Correctness by Construction course is available. Please access it at: https://wp.software.imdea.org/cbc/2026/03/16/second-exercise-sheet/ Deadline: Monday, April 6th, 2026. 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

Binary search & Rodin
by Manuel Carro 04 Mar '26

04 Mar '26

As usual, I have uploaded to the course web page the model that we developed during the last lecture. It is in the state in which only the proofs that are automatically discharged by Rodin upon saving the model are finished (green). I would like you to import that model in Rodin and finish the remaining proofs, either just selecting the PP prover and letting it do its job (using all hypotheses) or interacting with the prover, selecting a subset of the available hypotheses, when that is necessary. The slides contain a guide to do this for a particular case, but the scheme is similar for the other proofs in this model that need human intervention. Doing that by yourself will make you acquainted with the tool (which we will continue to use extensively during the course) and, in particular, with the interaction with theorem prover. FYI, there are some tips to discharge proofs at https://wp.software.imdea.org/cbc/proving-tips/ Not all of them are necessary at this moment, but we will be using many of them in due time! 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