- cbc - CLIPLab

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

Install Rodin and bring your laptops!
by Manuel Carro 21 Feb '24

21 Feb '24

Hi! I almost forgot to tell you... I plan to start working tomorrow (Wednesday, Feb. 22nd) with some simple examples and the development environment Rodin. So it would be great if you can bring your laptops *and* install Rodin. Please have a look at https://wp.software.imdea.org/cbc/rodin-installation-and-tips/ and follow the instruction installations there! Best, -- 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 0

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

2026

2025

2024

2023

2022

2021

2020

cbc