cbc February 2023

cbc@software.imdea.org

1 participants
3 discussions

First Event-B Homework
by Manuel 26 Feb '23

26 Feb '23

Hi, everyone. The first Event-B homework has been posted at https://wp.software.imdea.org/cbc/2023/02/20/first-event-b-homework-2/ Deadline: Tuesday February 28th, 23:59. Please don't hesitate to write me if you have questions. Also, please be sure to read the homework carefully before this Wednesday's lecture so that we can clarify any doubts at that time. Best regards, Manuel

2 1

Model from yesterday's lecture
by Manuel Carro 23 Feb '23

23 Feb '23

Dear all, the slides and the model from yesterday's lecture are available at the course's website. As suggested, please do the following: - Import it into Rodin. - Check that the proof obligations for models m0 and m1 are all discharged (i.e., in green). If not, click on the undischarged ones, switch to theorem prover view and use the "PP" button to discharge then. - Do the same for the proof obligations in machine m2. Some of the undischarged proofs can be proven this way, but others will need more (manual) intervention. Please refer to https://wp.software.imdea.org/cbc/rodin-installation-and-tips/ for basic instructions and to https://wp.software.imdea.org/cbc/proving-tips/#proving to learn more about what is available in the "Proving perspective". 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 0

Installing Rodin
by Manuel Carro 14 Feb '23

14 Feb '23

It is very likely that we will start using Rodin in the next lecture (Wed, 16th). Therefore I ask you to follow the instructions at https://wp.software.imdea.org/cbc/rodin-installation-and-tips/ and https://wp.software.imdea.org/cbc/#tools to download and install it. Please come to the lecture with laptops and batteries as full as possible (sometimes there are no cable extensions available, although I will try to have some of them in the lecture room). 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 0

2025

2024

2023

2022

2021

2020

cbc February 2023