- cbc - software.imdea.org

Homework deadline - today 4pm
by Manuel Carro 10 Mar '21

10 Mar '21

This is a gentle reminder that the deadline to turn in the first homework expires in 4 hours. I have only received homework from ten of you so far. I have replied to all of them. If any of you sent me your homework and did not get a reply from me, please let me know (and, to make things easier for me, please resend it). Also, please remember *not* to forward your homework to the cbc@... list. It's very easy to hit "Reply All" by mistake. "Reply All" is in most cases the right option; but not in this particular situation! 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

Lecture this Wednesday, March 3
by Manuel Carro 01 Mar '21

01 Mar '21

Hi, everyone. As I mentioned during the last lecture, we will be using the Rodin tool this week. Please go to https://wp.software.imdea.org/cbc/rodin-installation-and-tips/ and follow the instructions there. Make sure your installation starts up. If it doesn't, please post _to this list_: if your question reaches other classmates, perhaps they can help you to find a solution. It'd be also great if you could familiarize yourselves with Rodin a bit, so that we are as agile as possible during the lecture: you will have to use the tool together with me. One final thing: I have a meeting from 3pm to 4pm this Wednesday. It may be the case that it takes some more time. In that case, I ask you to please wait for some minutes until I can join the Zoom room. 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

CbyC: First homework
by Manuel Carro 25 Feb '21

25 Feb '21

The first homework for the Correctness by Construction course is available at https://wp.software.imdea.org/cbc/2021/02/25/first-event-b-homework/ 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

CbyC: slides & video
by Manuel Carro 11 Feb '21

11 Feb '21

Links to slides & video for Feb 10's session are available @ the course website (https://wp.software.imdea.org/cbc/). The password to access the video is the same we used for the zoom session. 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

Correctness by Construction: connection data for today's lecture
by Manuel 10 Feb '21

10 Feb '21

Hello everyone. The first lecture of the the Correctness by Construction course will take place today, February Wednesday 10, via Zoom. Please connect using the following data: https://zoom.us/j/9911012202 Password: CbyC Time: 4pm to 7pm The Zoom room will be available half an hour before the starting of the lecture in case you want to test your setup and make sure you can connect. I strongly advise to download the desktop application, rather than relying on the web-based interface. Please let you classmates know in case you think some of them is not reading / not receiving emails. Best regards, -- +-----------------------------------------------------------------------------+ | 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

Correctness by Construction: connection data for today's lecture
by Manuel 10 Feb '21

10 Feb '21

Hello everyone. The first lecture of the the Correctness by Construction course will take place today, February Wednesday 10, via Zoom. Please connect using the following data: https://zoom.us/j/9911012202 Password: CbyC Time: 4pm to 7pm The Zoom room will be available half an hour before the starting of the lecture in case you want to test your setup and make sure you can connect. I strongly advise to download the desktop application, rather than relying on the web-based interface. Please let you classmates know in case you think some of them is not reading / not receiving emails. Best regards, -- +-----------------------------------------------------------------------------+ | 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

Anonymous Doodle created and sent
by Manuel Carro 27 May '20

27 May '20

Dear all, you should have received three emails from no_reply(a)doodle.org with a link to vote for the presentations made by each other group -- please check your 'spam' folder in case they have been stored there. The deadline to vote is until tomorrow afternoon. The poll results cannot be observed until then. Thanks for your collaboration! 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

Today's session
by Manuel Carro 27 May '20

27 May '20

Hi. I think I had not sent you the links for today's session: https://zoom.us/j/7911012202 Passwd: 26404152 Again, from 3pm to 6pm. See you! -- 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 (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

2025

2024

2023

2022

2021

2020

cbc