- cbc - CLIPLab

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

Problems with automatic proving in Rodin
by Ignacio Ballesteros 26 Feb '20

26 Feb '20

Hi! At the end of the class some of us were having problems with automatic proving in Rodin. We were supposed to have installed Rodin Version: 3.4.0 and then install Atelier B Provers through "Help > Install New Software". I did that steps but it didn't work, Proof Obligations were still in brown. I just tried to install again Atelier B Provers, and this time, a popup appear after agreeing terms of service asking if "I was really sure to install that software". This popup didn't appear in previous installations. After accepting (and a suggested restart), proofs were passing. I don't know if this may be a solution for the ones who also have this same problem, but maybe double-checking that Atelier is installed can help. Ignacio. Just to make sure, these are my software versions: - Linux 5.5.5-arch1-1 _Name Version Id Provider_ Atelier B provers 2.2.1.r16701 com.clearsy.atelierb.provers.feature.group ClearSy Rodin Handbook v.2.5 2.5.0.201606291411 org.rodinp.handbook.feature.feature.group Formal Mind GmbH Rodin Platform 3.4.0.201802230927-6980ca1 org.rodinp.platform.product null Event-B Modeling Environment 3.4.0.201802230927-6980ca1 org.eventb.ide.feature.group ETH Zurich Rodin Platform Feature 3.4.0.201802230927-6980ca1 org.rodinp.platform.feature.group ETH Zurich You can make sure of installed versions going to "Help > About Rodin Platform > Installation Details"

2 1

Reminders for tomorrow
by Manuel Carro 25 Feb '20

25 Feb '20

Hi. This is a reminder for tomorrow's lecture: - The first homework is due tomorrow @ 3pm. Send me PDFs by mail. Scans of hand-written papers is OK. You can also hand me a physical page, but then you won't keep a copy. - Make sure you have a working Rodin installation. Refer to the slides at https://wp.software.imdea.org/cbc/wp-content/uploads/sites/5/2020/02/03-1-s… and follow the instructions in the section "Rodin: the Event B modeling tool". - Bring a laptop with Rodin working, because I intend for you to use it in class. 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

2026

2025

2024

2023

2022

2021

2020

cbc