cbc April 2020

cbc@software.imdea.org

1 participants
3 discussions

Start a nNew thread

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

2025

2024

2023

2022

2021

2020

cbc April 2020