Automata, Games, and Verification

Dear All, I’d like to draw your attention to a seminar on hyperproperties we are offering during the upcoming summer term.

In AG&V, we considered a system as correct if all its execution traces belong to a specified set of correct traces; hyperproperties generalize this from individual execution traces to sets of traces. Hyperproperties can reason about information-flow security (“an attacker cannot observe differences between traces that reveal secret information”) and notions like causality (“if the cause had not happened, the effect would not have happened”) or robustness (“small changes in the input result in small changes in the output”). In the seminar, we will look at current research on hyperproperties. We’ll discuss logics and verification algorithms, some of which may feel familiar after AG&V, and applications in security and elsewhere.

If you’re interested, more information is available on the seminar website (https://cms.cispa.saarland/hyper_23/); registration is open until April 12th, 23:59 CET, via the central seminar assignment system (https://seminars.cs.uni-saarland.de/sose23seminars).

Dear all, below are the details for the re-exam on March 28:

• The re-exam will take place on Tuesday, March 28, at 2:15 pm in HS002 (building E1 3). Please try to arrive a few minutes early.
• You must register via LSF at least a week before the exam. Please let us know immediately if you cannot register for some reason.  
• The re-exam will have a similar structure and guidelines as the first exam. That is: You will have 120 minutes to complete the exam; The exam is open book and you are allowed to use any written or printed material. 
• The content of all lectures and all problem sets is relevant to the exam. Material in the lecture notes that we will not have had time to cover during the lectures is not required for the exam.

• Please bring your student ID and a black or blue non-erasable pen.

Good luck! 

Thanks, everyone, for a great final round of discussion sessions! Here are a few points that came up today:

1. Extra office hour on Monday: There will be an additional office hour on Monday, Feb 13, 9-11 am. 
2. The exam on Tuesday: The exam will consist of four problems; the first problem consists of several true/false questions in the style of our warm-up questions; the other three problems will be in the style of the exercises on the problem sets. 
3. The co-Büchi condition: Several people noticed that we never formally defined the co-Büchi condition, which is the dual of the Büchi condition. The co-Büchi condition requires that a certain set of states only occurs finitely often. Formally, co-Büchi(F)= {α∈Q^ω | Inf(α) ∩ F = ∅}.

If any further questions come up, don’t hesitate to send us eMail or to stop by during the extra office hour on Monday. We wish you lots of success in the exam! See you on Tuesday!

Dear all, here are a few details regarding the exam on February 14. Please don't hesitate to let us know if you have further questions.

• The exam will take place on Tuesday, February 14, at 2:15 pm in HS002 (building E1 3). Please try to arrive a few minutes early.
• You must be registered via LSF at least a week before the exam. Please let us know immediately if you cannot register for some reason.  
• You will have 120 minutes to complete the exam.
• The exam is open book, i.e., you are allowed to use any written or printed material.
• The content of all lectures and all problem sets is relevant for the exam. Material in the lecture notes that we will not have had time to cover during the lectures is not required for the exam (but this is still great stuff, and you are highly encouraged to read the entire lecture notes).

• Please bring your student ID and a black or blue non-erasable pen.

Dear All, In a really unfortunate twist, both Hadar and I fell sick this morning. Since neither of us can give the lecture today, we, unfortunately, have to cancel today's lecture. There will also be no discussion sessions this week. The office hour on Thursday will be online only. Next week, everything should be back to normal. We are also planning to have a final discussion session on February 10. 

We suggest you use the extra time this week to review the course materials in preparation for our exam on February 14 and to let us know about any questions that come up. We're happy to answer your questions by email; if there are topics of common interest, we'll also pick them up in the lecture next week. Again, our apologies for cancelling today -- see you soon, stay healthy!

Dear All, Warm-up Questions & Problem Set 11 are now online. If you have not yet had a chance to fill out the course evaluation, please be sure to visit the link to the qualis website, which is available in the Materials section: we are excited to hear whether you liked the course! Thanks a lot for your time and effort, your comments are highly appreciated. See you on Friday!

Dear All, During the discussion session today, we discovered that the precedence order on the LTL operators defined in the lecture notes does not match what you may know from popular textbooks like Baier/Katoen. We decided to change the precedence rules in the lecture notes so that unary operators bind stronger than binary operators, Until takes precedence over conjunction, and negation and Next bind equally strongly. Sorry for the confusion! Note that this change affects the interpretation of the formulas in Warm-up Question 4 from the current set of questions. The updated lecture notes are available under Materials, together with a list of all changes we made since the beginning of the course. Thanks for the discussions today, have a great weekend!

Dear All, Warm-up Questions and Problem Set 7 are ready for your enjoyment! Also, please note that we will only have online meetings during the week before and after the break. At today's lecture, we discussed the following schedule for the next few weeks. See you on Friday!

Hi all, As some of you already noticed, Exercise 1.b in Problem Set 5 generates a big automaton. To make it a little less overwhelming, I slightly updated the exercise! Even though the difference is almost invisible (can you find it ? :)) it should make a big difference in the number of states! Enjoy!

The third problem set and the warm-up questions for Friday are available for download. This week's in-person discussion sessions will be in rooms 1.11 and 1.14 (building E1 1), online sessions at the usual zoom link. As usual, please let us know in case you cannot make it. See you on Friday! 

Dear All, You should now see your assigned discussion session on your personal status page. Please check and let us know if your assignment is missing or if the time slot does not work for you. We start this Friday (Nov 4th). In-person sessions will meet this week in building E1 1, room 1.14; to join an online session, please use the standard zoom link from the lecture (Information/Zoom Meeting). Please answer the warm-up questions before the session and bring your answers with you. See you on Friday!

Dear All, Thanks for a great first course meeting today! The first set of warm-up questions and the first problem set are now available in the "Materials" section. Also, please book the time slot for your discussion session at terminplaner6.dfn.de/b/0763239517732f0714f54c6493283ccc-48879. Please make your choice by the end of the week (31.10.2022, 00:00). 

If none of the offered time slots work for you, or if you run into any other problems, let us know. (If you previously entered your preferences on your personal status page, please make your choice again via the DFN link. Unfortunately, there was a glitch in the system, which did not show you all options.)  

The first discussion sessions will take place on Nov 4. The first office hour is already on Oct 27. Because of the holiday next week, the next lecture will be on Nov 8. See you soon!