cbc March 2026

cbc@software.imdea.org

1 participants
3 discussions

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 March 2026