cbc March 2026

cbc@software.imdea.org

1 participants
2 discussions

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