- cbc - CLIPLab

This post is a test
by Manuel Carro 27 Jan '25

27 Jan '25

I want to check if external users can successfully post.

1 0

Re: Welcome to the "cbc" mailing list
by Manuel Carro 27 Jan '25

27 Jan '25

This one goes to cbc(a)... On Mon, Jan 27, 2025 at 5:28 PM Manuel Carro <carro.manuel(a)gmail.com> wrote: > Thanks, professor! > > On Mon, Jan 27, 2025 at 5:26 PM <cbc-request(a)software.imdea.org> wrote: > >> >> 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. This 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 >> this course know that this message has been sent. >> >> The lectures will take place in the Montegancedo Campus of UPM on >> Wednesdays from 3pm to 6pm at classroom 6205 (building 6, level 2, >> room 05). >> >> The first lecture will take place on *February 5th*. >> >> Best, >> >> Manuel Carro >> >

1 0

Presentation slots for term project
by Manuel Carro 20 May '24

20 May '24

Dear all, please find here the suggested presentation slots for next Wednesday, according to the availability you told me: ErAusmus 3:30-3:50 The Burghers of Calais 3:50-4:10 Cbc-JAS 4:20-4:40 MUSS_24 4:40-5:00 RushGroup 5:10-5:30 TheoremProvers 5:30-5:50 Formal Methods 6:00-6:20 CEGroup 6:20-6:40 PPMasters 6:50-7:10 AMN 7:10-7:30 EMSE 7:40-8:00 Please let me know if that is OK for you or not. Every presentation has 20 minutes max. and there is an additional 10-minute gap every two presentations to serve as a buffer in case there are delays for any reason and to take a break every three or four presentations. Of course, you do not need to come early / stay until the end of the presentations if that is not possible for you. 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

Term project 2024
by Manuel Carro 28 Apr '24

28 Apr '24

Hi! The term project is available at https://wp.software.imdea.org/cbc/2024/04/28/term-project-2/ Let me know of any doubts, etc. you may have. 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

Today's lecture suspended
by Manuel Carro 24 Apr '24

24 Apr '24

Hi. I am afraid I will have to suspend today's lecture. I have been feeling sick and I don't think I will be in a condition to teach this evening. My apologies for any inconvenience that this may cause! Let us meet again in the next lecture on May 8th. If there are any questions or doubts regarding the homework or the course material, I will of course be happy to answer them over email. 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

Updated "Cars in a narrow bridge" slides
by Manuel Carro 18 Apr '24

18 Apr '24

Hi. Yesterday I was asked how the calculation of the variant in the "Cars in a Narrow Bridge" example was done. We did it during the lecture, and I have updated the slides to sketch how I did. 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

Fwd: Planning the presentation of the term project
by Manuel Carro 11 Apr '24

11 Apr '24

For those who have not yet signed up at https://docs.google.com/spreadsheets/d/1BTdeDeLeFBbUbxxj-6xEdQY5odPkPS6IROe… a gentle reminder. If you have troubles finding people to make a group, you can of course use this mailing list to look for group mates. Note that the messages are moderated, so they won't immediately be forwarded to everyone. Best / Saludos, Manuel -------------------- Start of forwarded message -------------------- From: Manuel Carro <manuel.carro(a)imdea.org> To: Correctness by Construction <cbc(a)software.imdea.org> Date: Mon, 08 Apr 2024 19:42:16 +0200 Subject: [cbc] Planning the presentation of the term project 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 | _______________________________________________ cbc mailing list cbc(a)software.imdea.org https://software.imdea.org/mailman/listinfo/cbc -------------------- End of forwarded message -------------------- -- +-----------------------------------------------------------------------------+ | 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

Third homework
by Manuel Carro 08 Apr '24

08 Apr '24

The third homework for Event B has been posted. Please find it here: https://wp.software.imdea.org/cbc/2024/04/08/third-homework-2/ Best / Saludos, -- +-----------------------------------------------------------------------------+ | 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

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

2026

2025

2024

2023

2022

2021

2020

cbc