- cbc - software.imdea.org

Welcome to the Correctness by Construction course!
by Manuel Carro 27 Jan '24

27 Jan '24

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/ Please read it thoroughly and let me know if there is something unclear (or just wrong). You can send messages to the mailing list using the address cbc(a)software.imdea.org Messages to the mailing list will reach *all* of your classmates. You are free to use it, but only for messages that can be read by everyone. The mailing list uses the official mail addresses provided by the university where you registered. Please make sure you read it frequently. Please also 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 on Wednesdays from 4pm to 7pm at classroom 6205 (building 6, level 2, room 05). The first lecture will take place on *February 7th*. This somewhat late date which is due to the need to synchronize with the MUSS master program, which starts later than other master programs. 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 15 May '23

15 May '23

Hi. The problem to be solved for the term project is available at https://wp.software.imdea.org/cbc/2023/04/18/term-project/. Please have a look at it! Important dates: - Send data for each team: Wednesday, May 3rd. - Deadline to send in all the material: Tuesday, May 16th, 23:59. - Presentations: May 17th, 16:00-19:00. Let me know if you have doubts, questions, etc. 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 1

Term Project: Looking for a team
by Janek Wenning 02 May '23

02 May '23

Hello everyone, if there are any teams looking for additional members or other people who are looking to form a team for the term project, I would love to hear back from you! Best regards, Janek

3 2

Second Event-B Homework
by Manuel Carro 17 Apr '23

17 Apr '23

Hi. The second homework for Event B has been released. Please consult it at https://wp.software.imdea.org/cbc/2023/03/31/second-event-b-homework/ As usual: - Write me in case there is anything you do not understand. - Feel free to write to the class mailing list, so if anyone has a question of general interest, please feel free to ask it openly. Please remember as well that the class mailing list reaches everyone in the course, so be careful regarding what information is disclosed. 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 1

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

2025

2024

2023

2022

2021

2020

cbc