- cbc - IMDEA Software

[Manuel Carro] Re: Plans for the rest of the term
by Manuel Carro 05 May '20

05 May '20

Just a reminder: please fill in the doodle. Only two of you answered so far. -- Manuel Carro : manuel.carro(a){imdea.org,upm.es} Director, IMDEA Software Institute : http://software.imdea.org Associate Professor, School of CS, UPM : http://www.fi.upm.es EIT Digital Spain : http://www.eitdigital.eu Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

Plans for the rest of the term
by Manuel Carro 04 May '20

04 May '20

Hi, everyone. I hope that you all are OK. In our last lecture I mentioned that the plan for the rest of the term was contingent on other courses: a professor who was also going to continue with the last part of CbC had to take care of another professor's lecture. This has not changed, and I will continue with CbC for the rest of the term. My proposal is to finish the term and evaluate the course with the homework so far plus the term project presentation (as I said, in groups of 2-3 people). The UPM Spring examination period is Thu, May 28th to Fri, June 12th, but we do not need to stick to it. If you have other exams to do / homework to hand in during that period, it may be better for you to be done earlier with CbC so that you can focus on other tasks. My proposal is to make the project presentations on Wed, May 27th, during the regular lecture slot. That will give you 3 solid weeks to work on it (it is more than enough). We would have lectures on May 6th and 13th and leave May 20th free in case there are any questions, clarifications, etc. Please let me know if you are OK or not with this plan, either answering to the list or replying privately to me. I very much prefer to agree on the presentation dates before sending the term project statement so that they appear in the document. Best regards, -- Manuel Carro : manuel.carro(a){imdea.org,upm.es} Director, IMDEA Software Institute : http://software.imdea.org Associate Professor, School of CS, UPM : http://www.fi.upm.es EIT Digital Spain : http://www.eitdigital.eu Madrid, Spain : +34-91-101-2202 ext. 4140

1 1

Correctness by Construction: Lecture today
by Manuel 22 Apr '20

22 Apr '20

3pm to 6pm, as usual, at https://zoom.us/j/7911012202

1 0

Lecture today @ 3pm!
by Manuel Carro 15 Apr '20

15 Apr '20

Hi, all. We'll have lecture today @ 3pm, as usual! Lecture room: https://zoom.us/j/7911012202 I'm not using a pwd @ the moment. If we are zoombombed, I'll change the policy. Best, Manuel -- +-----------------------------------------------------------------------------+ | 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

Second remote session - followup
by Manuel Carro 01 Apr '20

01 Apr '20

Hi, all. I have updated the course web page with entries for the last session (slides, model, recording). As usual, I'll let you know of the URL for the next session (Wed, March 25th). In the meantime, some outstanding issues: - Hermenegildo: you are not alone with the 32-bit issue in Mac OS Catalina: https://sourceforge.net/p/rodin-b-sharp/mailman/message/36868847/ A possible workaround is using SMT solvers instead of the PP theorem prover (assuming they are 64-bit binaries). Go to Help -> Install new software, deinstall the Atelier B provers, in the "Work with" pull-down menu select Rodin - http://rodin-b-sharp.sourceforge.net/updates Scroll down to "Prover extensions", expand the entry, select "SMT Solvers" (latest version), install it, restart. In the Proving Perspective, a new "SMT" button should appear. I do not have a lot of experience with it, but I assume it also works with the hypotheses that appear in the "Selected Hypotheses" subwindow. In my limited experience, it works quite well. I have seen cases where PP does not straightforwardly solve issues that SMT does, and the other way around. I was not planning to use them in the course because I did not want to introduce additional ingredients, but having one possibility is better than none. - Shuting: were the POs of m1 (with the variant-related proofs) finally discharged? They should have... I looked again at the goals that were pending and they were definitely provable. If you did not manage to discharge the POs, please try again clicking in the prover: - pp (and wait until it fails) - p1 (and wait as well) - ml (it is better than pp in a few cases, but pp should be more than enough for this problem) - Lucy: I redid the relative deadlock freedom from scratch and I also had to go to the theorem prover. I am convinced I did not have to do at some time. It may have to do with Rodin saving previous proof strategies and reusing them. - Adrian: could you follow the lecture? IIRC you were using connecting using your cell phone. If it was troublesome, we can try to find a workaround. - Someone else had troubles / issues, but I do not remember who that was... - Last: I am still expecting HW#2 from some of you. If you are facing difficulties, please let me know. Best, -- Manuel Carro : manuel.carro(a){imdea.org,upm.es} Director, IMDEA Software Institute : http://software.imdea.org Associate Professor, School of CS, UPM : http://www.fi.upm.es EIT Digital Spain : http://www.eitdigital.eu Madrid, Spain : +34-91-101-2202 ext. 4140

1 2

Technical support for #VenceAlVirus
by Manuel Carro 29 Mar '20

29 Mar '20

Dear friends, this mail is to look for volunteers who can help during the #VenceAlVirus hackathon. Please Google the tag if you do not know what I am talking about. Good Spanish command is essential; that is why the rest of the message is in Spanish. If you are not able to follow it, then this message is probably not for you :-/ --------------------------------------------------------------------------- La Comunidad de Madrid ha empujado la celebración del Hackathon virtual #VenceAlVirus . Se abrirá el próximo martes 31 y tendrá varias fases que culminarán el lunes 13 de abril; todos estáis invitados a participar. Para la interacción entre los participantes y con la organización se ha puesto a disposición de todos una instalación de Taiga, una plataforma de planificación de proyectos, y MatterMost, una plataforma de comunicación, ambas de código abierto. [*] Aunque se espera que la mayor parte de los participantes las utilicen de manera autónoma o usen sus propios medios de organización, se prevé que la entrega de resultados y la comunicación con la organización se lleven a cabo a través de esas plataformas. Por eso es de esperar que surjan dudas técnicas sobre las mismas y su uso, necesidades de administración (p.e., creación de canales, seguimiento de características de proyectos) y monitorización (p.e., moderación de canales para asegurar una buena convivencia). Estamos buscando voluntarios que puedan emplear parte de su tiempo en estas tareas. La experiencia previa con Taiga y Mattermost es lo más deseable, pero si tienes experiencia con herramientas suficientemente similares, también puedes ser útil. Si quieres participar, rellena por favor el formulario en https://forms.gle/az2o4MoruuuMYRv18 para que nos podamos poner en contacto contigo. Algunas aclaraciones: - Lamentablemente no puedo asegurar que pueda responder a preguntas directas a este correo: voy a estar un poco sobrecargado. - No usaremos tus datos más que para seleccionar voluntarios. - Es posible que no nos pongamos en contacto inmediatamente contigo. Es más, es posible que nos pongamos en contacto con voluntarios mientras el hackathon está en marcha para suplir posibles bajas, necesidades específicas, etc. - Aunque el esfuerzo de todos es esencial en este momento, no queremos que tus quehaceres habituales se vean perturbados. Asegúrate de que tus responsables (jefes de proyecto, directores de tesis, jefes de departamento, etc.) están de acuerdo en tu participación si crees que puedes necesitar tiempo que usualmente emplearías en tareas relacionadas con tu trabajo. Por supuesto, difunde este mensaje entre quienes crees que pueden estar interesados en colaborar. [*] Mil gracias a Pablo Ruiz (Kaleidos/Taiga) y Jesús Espino (MatterMost) por su tiempo y ayuda en la instalación de las herramientas - Kudos! -- Manuel Carro : manuel.carro(a){imdea.org,upm.es} Director, IMDEA Software Institute : http://software.imdea.org Associate Professor, School of CS, UPM : http://www.fi.upm.es EIT Digital Spain : http://www.eitdigital.eu Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

First remote session
by Manuel Carro 17 Mar '20

17 Mar '20

Hi, all. Thanks for your attendance yesterday. I have left at the course website (https://wp.software.imdea.org/cbc/) the slides used so far, the recording of the lecture, and the model built so far (for you to check). If the recording does not play in your browser, just download it. As we discussed during the lecture: - Please give me feedback on how it went for you. In particular, was two hours too long / ok / could have been longer? Any idea on how to improve the experience? - Next week was a no-lecture period at UPM (but not at UAM / UCM) for student activities. However, since they have been cancelled, it looks like we can have a session. Please let me know if this is OK to you -- you may have made plans; but it is also likely that these plans have been cancelled. - Please remember that there is a homework deadline on March 18th. On a related topic, the link that Lucy shared (https://medium.com/@tomaspueyo/coronavirus-act-today-or-people-will-die-f4d…) points to a good report. I have been told that the French government is using it to decide policies. Best regards, Manuel -- +-----------------------------------------------------------------------------+ | 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

***SPAM*** Coronavirus alert
by Manuel Carro 11 Mar '20

11 Mar '20

Dear all, I assume you all are aware of the latest news related to the coronavirus in Madrid: Universities (and all the schools, actually) will be closed until March 26th, Thu. While we do not lecture at the University, I think that I should follow the order: coming to the campus also potentially exposes you to the virus due to public transportation. So we won't have lectures for at least three weeks. I was planning to do hands-on sessions with Rodin with lots of explanations on the process. Since that does not lend itself to self-study, I will make slides on other parts of the course that can be independently studied to, at least, be able to advance somewhat. I will let you know when they are ready. 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

Homework and next session
by Manuel Carro 04 Mar '20

04 Mar '20

* The slides for today's session are on the web. * New homework has been posted. * Remember to bring a laptop with a working Rodin installation for the next lecture. You are going to use it a lot. Cheers, -- +-----------------------------------------------------------------------------+ | 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

Yesterday's session
by Manuel Carro 27 Feb '20

27 Feb '20

This is a followup to yesterday's session, especially for those who could not attend the 2nd half. We finished correcting most of the homework and we devoted part of the session to model the exercises in Rodin. We had time to do the "Odd way" to calculate n^2 only, as we bumped into some technical hurdles. I believe that the mail Ignacio sent sheds light on how to solve the problem. Please howl if that is not the case. For those who attended the full lecture: please model on your own the Russian multiplication in Rodin, including correctness and termination (as we did in th "Odd n^2". Note: Rodin has 'mod' among the arithmetic operators. Some invariant may not be proven straight away. Nothing to worry about, and this it can be different for each of you. There are reasons for that - more on it in the next session and the cure is easy. For those who did not do that last part: *please* make sure to install Rodin as per the instructions in the last set of slides, import the IntegerDivision example to see what a model and the editor looks like, and try to model the n^2 and the Russian multiplication calculations. In the next session I plan to show something with the Russian multiplication example and I would like you to be up-to-date with it. And in coming sessions ad homeworks I plan you to use Rodin extensively. Rodin can be initially disconcerting, but it is only 10 minutes until one understands how the editor works. I suggest that your pair up with some of your classmates for a quick primer. Ask in the mailing list if you experience problems. 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