- cbc - software.imdea.org

Third Event-B Homework
by Manuel Carro 14 Apr '23

14 Apr '23

Hi, everyone. I have posted the third Event-B homework; please check the course's website or download it directly from https://wp.software.imdea.org/cbc/wp-content/uploads/sites/5/2023/04/03-one… Deadline: Wednesday, May 3rd 2023, 15:59, . 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

No lecture today (22/03/2022)
by Manuel Carro 22 Mar '23

22 Mar '23

Dear all, I am feeling rather unwell today, and I do not think I will be able to teach this afternoon's lecture. So I believe it is best to cancel it, so that you don't have to come to the campus for something that may not take place. I am sorry about this late announcement; please let your classmates know if you have other forms of contact with them in case they cannot read this email. 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

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

Welcome to Correctness by Construction
by Manuel Carro 29 Jan '23

29 Jan '23

Hi. If you receive this email, you have registered for the Correctness by Construction course. It is taught in three different master programs: MFII, EMSE, and MUSS, plus it is part of eligible requirements for the DSSC PhD program. The mailing list and the web page will be our primary communication means outside the classroom. The web page is located at https://wp.software.imdea.org/cbc/ and you can send messages to the mailing list using the address cbc(a)software.imdea.org Note that a message to the mailing list can reach *all* of your classmates. You are free to use it, but only for messages that should reach all of them. The mailing list uses the official mail addresses provided by the universities where you registered. Please make sure you read it frequently. Please let your classmates who are registered in CbC know that this message has been sent. The lectures will take place in the Montegancedo Campus of UPM every Wednesday from 4pm to 7pm at classroom 6306 (building 6, level 3, room 06). The first lecture will take place next Wednesday, February 1st. 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

Slides / model for the lecture on May 11th
by Manuel Carro 15 May '22

15 May '22

Hi. I have just posted the material for the last lecture. Sorry it took so long, but I did not like that the material was half-cooked and I spent some time polishing the mode and the proofs, in the hope that it is ore useful. 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

Extension for HW#3
by Manuel Carro 03 May '22

03 May '22

Dear all, I have received some requests to extend the deadline to turn in HW#3. However, a number of you have already submitted it, and it would be unfair to give a extension when some of you are / have been working on the homework, perhaps prioritizing it over other tasks. Therefore I believe that an adequate possibility would be as follows: - The deadline to turn in HW#3 is extended until Friday, May 6, 23:59. - The maximum grade, on a scale of 0 to 10, that can be obtained with this homework will be capped as follows: - If you turn it in by this Wednesday, May 4th, 15:59, you can have a maximum grade of 10 (out of 10). - Similarly, for Wednesday May 4th, by 23:59, the max. grade is 8.5. - Thursday May 5th, by 11:59: 7.0 - Thursday May 5th, by 23:59: 5.5 - Friday May 6th, by 11:59: 4.0 - Friday May 6th, by 23:59: 2.5 - Later than Friday May 6th, 23:50: 0.0 For example, if someone sends in the homework on Thursday at 10pm and the evaluation of the homework is an 8.0, the grade to be received would be 5.5. 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

Term project
by Manuel Carro 02 May '22

02 May '22

Hi. The term project is available at https://wp.software.imdea.org/cbc/2022/05/02/project-term-robot-arms/ Important dates: - Deadline to send me the names of the group components: Wednesday, May 4th. - Deadline to send me the project material (please see the term project statement): Tuesday, May 24th, 23:59. - Presentation session: Wednesday, May 25th, 4pm to 7 pm. 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

Plans for the rest of course
by Manuel Carro 27 Apr '22

27 Apr '22

Dear all, as we discussed today during the lecture, we will continue with Event-B during the rest of the course. I will make the term project available in short. The project is to be made in groups of *three* people and presented in a session. In order to free you as soon as possible and give you time to prepare other exams / homework, etc., we agreed to schedule the presentation of the project solutions for May, Wed 25th (approx. one month from now), in the same place and time slot we use for the lectures. Therefore: - If that date & time is NOT feasible for you, please let me know ASAP and, in any case, *before* next Wednesday (May 4). - Please set up groups of three people and send me (before next Wednesday) the names of the members of each group. If you are not able to make a 3-person group, please let me know ASAP (again, before next Wednesday) to look for a solution. 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

2026

2025

2024

2023

2022

2021

2020

cbc