cbc March 2020

cbc@software.imdea.org

1 participants
5 discussions

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

2025

2024

2023

2022

2021

2020

cbc March 2020