- cbc - CLIPLab

Today's (Wed. 20) lecture
by Manuel Carro 20 May '20

20 May '20

Hi. Since today's lecture did not cover material but question, I think it ought not to go online on the web. You can, however, access it here: https://software.imdea.org/cloud/index.php/s/aaS3ZRg32w2GXig I am afraid I did not record the first question; sorry about that... 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 0

Today's session & model checking
by Manuel Carro 20 May '20

20 May '20

I've had a quick look @ the model checking options. What I understand it does with the constants is: - It makes them range according to the values set for MAXINT and MININT. So, to explore more states, just increase these values. Note: checking time is likely to grow exponentially. - By default, these are enumerated orderly, starting at one. Since it stops when a problem is found, these are usually with a small value. If you want them to be explored in another order, you can check the box "Randomise enumeration of variables". But then, counterexamples won't use small values, which are often easier to deal with. 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 0

Session tomorrow?
by Manuel Carro 20 May '20

20 May '20

Hi, everyone. I have not received any request to have a session tomorrow. Please let me know if (any) of you would like to have one. Cheers, Manuel -- 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

Collaborate in Linux
by Manuel 17 May '20

17 May '20

Hi. Has any of you used Collaborate in Linux? I have seen instructions on the web, but they involved installing lots of components, including specific web browsers I had never heard about before. Best, Manuel

1 0

today's course
by Manuel Carro 11 May '20

11 May '20

Sorry I had forgotten to send the link for today: https://us02web.zoom.us/j/9911012202?pwd=NHRoOE1HcVhKYXkwS1NtNzdCZTBUQT09 It should take you stright to the meeting room. Otherwise: https://us02web.zoom.us/j/9911012202 Password: 25241661 -- 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

Comments to lecture of May 6, 2020
by Manuel Carro 06 May '20

06 May '20

You can get some information on contact tracing applications at - Out of curiosity, I tried Lucy's suggestion to use (mod 2) instead of the definition of parity(·). It didn't work for me: all theorem provers / SMT solvers stop trying to prove s ∈ ℕ ⊢ 1 - (s mod 2) = (s + 1) mod 2 which is precisely thee definition of parity I introduced as an axiom :-) This does not mean that theorem provers / SMT solvers are incredibly stupid. They have many compile-time configuration and invocation options and different theory modules that evolve and are improved continuously. It is possible that the matter is finding the right ones. - A good, recent summary to learn about the status of contact tracing applications is https://apnews.com/eb37b9ada939dfaff40925533c977b5c (but if you do a Google search, many hits will appear) The documents describing the DP3T proposal are at https://github.com/DP-3T/documents/blob/master/ , and the repositories under https://github.com/DP-3T have the source code. 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 0

Internet problems
by Manuel Carro 06 May '20

06 May '20

I am experiencing problems with my internet connection. Please hold on for some moments! ⁣Sent from phone. Please excuse brevity. Manuel Carro IMDEA Software Institute, director software.imdea.org Assoc. professor, Tech. Univ. of Madrid - UPM www.upm.es Sent from TypeApp

1 0

Today's lecture + next week's lecture
by Manuel Carro 06 May '20

06 May '20

Hi. For today's lecture from 3pm to 6pm, please the URL https://zoom.us/j/7911012202 Password: 10353613 For today's lecture, please have Rodin ready. We will build a small distributed system together. Most of you (one person did not answer the doodle yet) chose to have next week's lecture on Monday, 4pm to 7pm. Cheers, -- 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

[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

2026

2025

2024

2023

2022

2021

2020

cbc