cbc March 2024

cbc@software.imdea.org

1 participants
2 discussions

Proofs from today's lecture
by Manuel Carro 15 Mar '24

15 Mar '24

As you may remember, some proofs that were supposed to be discharged by the automatic theorem provers in Rodin today were not proven. I am not yet sure why, but, barring some mistake in the model that went unnoticed, it may be due to a different version of Rodin with different heuristics in the automatic theorem provers. For the remaining profs that should be proven, except those concerning invariant 5, what worked for me was: - Go to the Proving perspective, select one unproven proof obligation, double click on it. - In the left panel with the proof tree, cut (✀) / slash backtrack the search tree to the root, so that the proof three only contains the root. - Select "lasso" to bring to the current hypotheses a set of relevant formulas. In ny Rodin insallation, after this the automatic theorem prover is triggered and it performs a series of inference steps that end up proving the intended goal. 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 2

First CbC Homework
by Manuel Carro 02 Mar '24

02 Mar '24

Dear all, the first homework for Correctness by Construction is available at https://t.ly/WoFXr . Deadline: Tuesday March 5th, 23:59. 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 Board of Directors, Informatics Europe : https://www.informatics-europe.org/ Madrid, Spain : +34-91-101-2202 ext. 4140

1 1

2025

2024

2023

2022

2021

2020

cbc March 2024