- cbc - CLIPLab

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

Mismatch of Slides on Website
by Leyi Qiang 20 Feb '26

20 Feb '26

Hi Manuel, The slides "logic and inference rules" uploaded to the website for today’s lecture seem different from what you showed in class. Could you please double check them? Thank you. Bests, -- Leyi Qiang

2 1

First Exercise Sheet 2026
by Manuel Carro 16 Feb '26

16 Feb '26

Hi, all. The first exercise sheet is available. Please find the announcement and a link to the sheet here: https://wp.software.imdea.org/cbc/2026/02/16/first-exercise-sheet/ Deadline: February 27th, 2026, 23:59 (just before midnight). 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