- cbc - IMDEA Software

Planning the presentation of the term project
by Manuel Carro 08 Apr '24

08 Apr '24

Hello everyone. As I mentioned last week during the lecture, we should plan the presentation of the term project . I usually require groups of three people to work jointly on the project and make a presentation. According to the last homework submissions, I assume there will be 10 groups. The presentations can be squeezed in a 3-hour session, but it's too tight. The date for the regular / final exam is June 12th @ 3pm (and it can be retaken on July 3rd). Whoever passes the course with homework + term project does not need to go to the final exam. But everyone has the right to take that exam instead of the homework; and, of course, there may be people who do not pass with homework + project, and prefer to take the June exam instead of the July exam. So, June 12 has to be saved for this possibility. The last lecture is on May 22nd. The previous is on May 8th (May 15th is holidays), which is too early / far apart from 22nd. My proposal is either to: - Enlarge the session on May 22nd by taking one extra hour either before or after the regular session, or - Use around one hour or so on May 24th, Friday, to schedule some presentations there. [I assume that you have other lectures the rest of days of the week, so presenting on Monday / Tuesday / Thursday is not an option. Please let me know otherwise.] Therefore, I am asking you to please provide information regarding your availability on the 22nd and 24th days, as well as data for the groups for the term project. Please go to the Google Docs spreadsheet at https://docs.google.com/spreadsheets/d/1BTdeDeLeFBbUbxxj-6xEdQY5odPkPS6IROe… and: 1.- Fill in your name. 2.- State whether you could make a presentation on May Wed 22, one hour before or one hour after the regular lecture schedule, and/or on May Fri 24 sometime during the morning or the afternoon (we'd agree on the exact time later on). Please write down all your possibilities to have as much freedom as possible. 3.- When you know who are going to be in the group with you, give the group a name and associate the members of the group with that name. You can name your group "Group N" for some number, but some imagination won't hurt 😁. Please provide the information as early as it is possible for you, and *very* preferably before this Friday, April 12, EOB. Thanks! 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

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

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

2026

2025

2024

2023

2022

2021

2020

cbc