Exam structure, instructions, suggestions, and other useless information
Some info on the exam, which in my opinion is pretty useless, but if you find it comforting - great.
Material: everything we covered. In the notes: up to and including Section 13, excluding Theorem 13.2.
What you need to memorize:
- The different acceptance conditions for automata, including their acronyms (DPW, NRW, NBW, etc.)
- The syntax and semantics of LTL, S1S, and games.
There is not much else to memorize. I will assume you know and understand the various constructions we've seen, but this is more about understanding than memorizing.
- The exam will be *2 hours* long.
- It will consist of 4 questions. Some answers require proofs, but some will be very short (so there is not too much writing to do).
- The questions will resemble the homework in the sense that they will be questions about the material...
How to prepare:
- I don't know.
- Go over the material and the homework and think whether you understand it.
- If you have time, try to play around with definitions and ideas and ask yourself what would happen if this or that changes.
As usual, if you want to meet and ask questions, either come to my reception hour or email me to schedule another time. Or Piazza.
|פורסם ב- 29/6/2022, 22:15:56 Created on 29/6/2022, 22:15:56 Создано 29/6/2022, 22:15:56 تم النشر ب- 29/6/2022, 22:15:56|
Formal verification job advertisement
Avital Steinitz, a former colleague of mine, works at a company that does formal verification and automata related stuff.
He asked me to pass along a recruitment ad. See below the job description, in case you're interested.
Disclaimer: I am not affiliated with this company or this job in any way. Moreover, I have no information about what they actually do.
If you're interested and want to talk to Avital before applying, let me know and I'll connect you.
Lightlytics is a SaaS platform that helps companies code and deploy configurations faster and safer from plan to cloud. The platform creates a real-time simulated model, or “Cloud Twin”, of the production environments across the entire cloud-native stack that simulates all configuration changes. Developers and engineers can then use this model to automatically predict, preempt, and prevent critical business disruptions caused by infrastructure changes. DevOps teams and Ops teams depend on Lightlytics to increase confidence, reduce costs, and prevent downtime, data loss, and deployment delays. Gain confidence in every configuration at lightlytics.com.
We're growing and things are great. But there's just one thing missing: You!
We are looking for an experienced Algo Developer to join our Core R&D Group. Be part of our software architecture team, responsible for architecting, seeding, leading, and driving cloud-focused product features. You will join the fast paced, highly technical and savvy group in charge of building Lightlytics’s core and algorithms, while working with cutting edge technologies.
|עדכון אחרון ב- 27/6/2022, 10:10:50 Last updated on 27/6/2022, 10:10:50 Последняя модификация 27/6/2022, 10:10:50 تمت الحتلنة الأخيرة ب- 27/6/2022, 10:10:50|
COVID in class
I've been informed that one of the attendants in today's class was tested positive for COVID (after class).
Naturally, automata-oriented people have stronger immune system than "normies", but still - you may want to get tested.
Good health to all.
|פורסם ב- 26/6/2022, 17:08:00 Created on 26/6/2022, 17:08:00 Создано 26/6/2022, 17:08:00 تم النشر ب- 26/6/2022, 17:08:00|
Ex3 Grades and Feedback
Ex3 is returned.
The grades were lower than previous exercises. I strongly recommend you read my/each other's solutions, since there are some important ideas there.
As usual, if you want to discuss anything, let me know.
|פורסם ב- 20/6/2022, 14:12:23 Created on 20/6/2022, 14:12:23 Создано 20/6/2022, 14:12:23 تم النشر ب- 20/6/2022, 14:12:23|
The last exercise is online. It's a short one.
The due date is 26.6, so that it doesn't go beyond the semester.
If you need an extension, email me, but I recommend not to drag it out.
|פורסם ב- 19/6/2022, 09:50:22 Created on 19/6/2022, 09:50:22 Создано 19/6/2022, 09:50:22 تم النشر ب- 19/6/2022, 09:50:22|
A talk by Apple's formal verification team
The Apple verification team will be giving a talk next week. You may find it interesting.
See publication below (in Hebrew).
Disclaimer: I am not affiliated with Apple, nor with any other company (or fruit).
אפל מגיעה לקמפוס לשוחח לראשונה על אימות פורמלי, הגשר בין האקדמיה לתעשייה.
באירוע יציגו ארז גולן (מנהל הקבוצה) ואוהד דרוקר (מהנדס בקבוצה ודוקטור למתמטיקה) את ההיבט ההנדסי-לוגי כמו התאורטי-אקדמי מנקודת המבט של קבוצת האימותם הפורמלי בישראל.
בואו לפגוש אותנו ביום שלישי 21.6.22 בין השעות 18:00-20:00, בניין אמאדו חדר 232.
*מספר המקומות בהרצאה מוגבל, יש להירשם מראש ולקבל אישור הגעה באמצעותו ניתן להיכנס לאירוע.
|פורסם ב- 16/6/2022, 20:34:09 Created on 16/6/2022, 20:34:09 Создано 16/6/2022, 20:34:09 تم النشر ب- 16/6/2022, 20:34:09|
Office hour tomorrow - Cancelled
I'm afraid I have to cancel my office hour tomorrow (due to a strike in the preschool system).
If you want to schedule a meeting, email me.
|פורסם ב- 12/6/2022, 21:09:50 Created on 12/6/2022, 21:09:50 Создано 12/6/2022, 21:09:50 تم النشر ب- 12/6/2022, 21:09:50|
|Due to public demand, I'm giving a two-day extension on Ex3.|
Oh merciful me.
|פורסם ב- 11/6/2022, 21:47:25 Created on 11/6/2022, 21:47:25 Создано 11/6/2022, 21:47:25 تم النشر ب- 11/6/2022, 21:47:25|
Office hour next Monday
My office hour next week will be from 9:30 to 10:30 (30 min earlier than usual).
I hope this would not cause mass panic.
|פורסם ב- 8/6/2022, 11:12:10 Created on 8/6/2022, 11:12:10 Создано 8/6/2022, 11:12:10 تم النشر ب- 8/6/2022, 11:12:10|
Ex3 is online!
|Ex3 is online, due on 12.6.2022.|
Keep in mind that you will have all the necessary material to solve it by tomorrow, and that next week we'll move to different material.
So as usual, I recommend solving it early.
|פורסם ב- 28/5/2022, 21:49:12 Created on 28/5/2022, 21:49:12 Создано 28/5/2022, 21:49:12 تم النشر ب- 28/5/2022, 21:49:12|
Free access to FLoC! (in return for volunteering)
tl;dr: if you want to volunteer in FLoC, you can get free access:
As I mentioned a couple of times, during the summer we will host a multi-conference event called FLoC:
If you're interested in automata/logic/games/verification (which you obviously are), there will be interesting talks there, by the very best researchers in the field.
Registration is generally quite expensive, but if you volunteer, you get free access (and a T-shirt!)
This involves helping with registration, directions, moving microphones around, etc.
You can register in the link above if you're interested.
|פורסם ב- 22/5/2022, 15:07:17 Created on 22/5/2022, 15:07:17 Создано 22/5/2022, 15:07:17 تم النشر ب- 22/5/2022, 15:07:17|
Ex2 Grades and feedback
The feedback and grades for Ex2 are on the website.
Please read my comments in the file (they should be readable with Adobe Acrobat. Not sure about other readers).
Apologies that it took so long.
|פורסם ב- 19/5/2022, 20:55:29 Created on 19/5/2022, 20:55:29 Создано 19/5/2022, 20:55:29 تم النشر ب- 19/5/2022, 20:55:29|
|Ex2 solution is online.|
Let me know if you have any questions.
Reminder: reading the solution is part of the course requirements.
|פורסם ב- 12/5/2022, 11:47:39 Created on 12/5/2022, 11:47:39 Создано 12/5/2022, 11:47:39 تم النشر ب- 12/5/2022, 11:47:39|
Reception hour tomorrow (2.5.2022)
I'm unable to hold my usual reception hour tomorrow.
If you wanted to come, please email me and we'll either meet on Zoom or schedule a different hour.
|פורסם ב- 1/5/2022, 17:24:15 Created on 1/5/2022, 17:24:15 Создано 1/5/2022, 17:24:15 تم النشر ب- 1/5/2022, 17:24:15|
Ex2 is online!
|Ex2 is online, due on 8.5.2022.|
I recommend solving it before the lecture of 8.5, simply because that lecture won't be related to the exercise, so it's better if you don't have the exercise deadline looming.
As usual, please ask question/ discuss topics in Piazza.
|עדכון אחרון ב- 24/4/2022, 12:39:06 Last updated on 24/4/2022, 12:39:06 Последняя модификация 24/4/2022, 12:39:06 تمت الحتلنة الأخيرة ب- 24/4/2022, 12:39:06|
Ex1 Grades and Feedback
|Ex1 has been marked.|
I tried to give a detailed feedback, please go through it carefully.
Note that I didn't check the automata constructions of Q4 carefully. Please compare with my solution and ask if you see differences.
|פורסם ב- 16/4/2022, 23:20:25 Created on 16/4/2022, 23:20:25 Создано 16/4/2022, 23:20:25 تم النشر ب- 16/4/2022, 23:20:25|
The solution for Ex1 is online.
Note: I will assume you have read and understood the exercise solutions.
|פורסם ב- 16/4/2022, 19:51:51 Created on 16/4/2022, 19:51:51 Создано 16/4/2022, 19:51:51 تم النشر ب- 16/4/2022, 19:51:51|
Ex1 is online!
|Ex1 is online. Please read the submission guidelines in the exercise description.|
The exercise is meant to help you get comfortable with NBWs.
Questions can be posted on Piazza. I would be very happy to have interesting discussions there.
|עדכון אחרון ב- 27/3/2022, 09:57:47 Last updated on 27/3/2022, 09:57:47 Последняя модификация 27/3/2022, 09:57:47 تمت الحتلنة الأخيرة ب- 27/3/2022, 09:57:47|
Crash Course on Computability - Sunday 21:00 - 22:30
|The Crash Course on Computability and Complexity will take place on:|
Sunday, 27.3.2022, 21:00 - 22:30.
|פורסם ב- 22/3/2022, 15:43:14 Created on 22/3/2022, 15:43:14 Создано 22/3/2022, 15:43:14 تم النشر ب- 22/3/2022, 15:43:14|
Crash course in Computability and Complexity
|If you haven't taken computability yet, or if you feel like you want a refreshment, I will give a crash course (90min) containing most of the stuff we will need for the course.|
Please fill the Doodle link with convenient times (only if you plan on attending)
This will be on Zoom, and I will record it for later reference.
|פורסם ב- 20/3/2022, 12:45:30 Created on 20/3/2022, 12:45:30 Создано 20/3/2022, 12:45:30 تم النشر ب- 20/3/2022, 12:45:30|
Welcome to Automata, Logic and Games (ALG)!
ALG will start on Sunday, but we can all start getting excited today!
Please read the syllabus and FAQ on the course website, so you have a rough idea what to expect.
We'll discuss the administrative stuff in class. In the meantime, here's a link to Piazza forum for the course, where you can ask questions, discuss the material, etc.
Looking forward to seeing you all,
|פורסם ב- 18/3/2022, 15:11:05 Created on 18/3/2022, 15:11:05 Создано 18/3/2022, 15:11:05 تم النشر ب- 18/3/2022, 15:11:05|