|If you have not done so already, please contact the instructors to set up a date for presenting your final project.|
|פורסם ב- 2/9/2021, 09:04:40 Created on 2/9/2021, 09:04:40 Создано 2/9/2021, 09:04:40 تم النشر ب- 2/9/2021, 09:04:40|
We are collecting the URIs of all the Git repositories of ongoing projects. Please fill in this form:
We ask that you push your changes regularly so that we can monitor individual teams' progress effectively.
|פורסם ב- 30/5/2021, 13:47:18 Created on 30/5/2021, 13:47:18 Создано 30/5/2021, 13:47:18 تم النشر ب- 30/5/2021, 13:47:18|
How Spacer Works: Required Reference Material
|This week we will have a lecture on IC3/PDR, the mechanism that underlies invariant inference in Spacer (the thing you are translating the program to).|
That is, you will have a lecture; you are instructed to watch Yakir's lecture from 236642. You can ask us questions on Slack or schedule office hours.
You are also encouraged to tell us about your progress in the project and/or ask for guidance if you are not sure what to do next.
|פורסם ב- 30/5/2021, 12:21:27 Created on 30/5/2021, 12:21:27 Создано 30/5/2021, 12:21:27 تم النشر ب- 30/5/2021, 12:21:27|
Info for UI design
|As I said in the lecture, you are *very much* encouraged to create a small UI for your verifier.|
For ideas on how such a UI should look, visit https://rise4fun.com/dafny (also added to the "links" tab). Dafny is a software verification tool made by Microsoft Research, and it has a Web UI. You can experiment with it a little.
To help you get started, I have created a subdirectory `ref-src/ui` with some sample code in the project GitHub repository.
Feel free to be creative with your visual design.
|פורסם ב- 22/5/2021, 18:31:28 Created on 22/5/2021, 18:31:28 Создано 22/5/2021, 18:31:28 تم النشر ب- 22/5/2021, 18:31:28|
Lecture Today (May 4)
Today's lecture will be online only.
Sorry for the late notice.
See you virtually!
|פורסם ב- 4/5/2021, 15:43:50 Created on 4/5/2021, 15:43:50 Создано 4/5/2021, 15:43:50 تم النشر ب- 4/5/2021, 15:43:50|
Next project milestone
|Notice that the next milestone is scheduled to 18/5. Presentation will be in a similar format to last time; be prepared to also show us your benchmarks (example programs that your implementation runs on).|
As usual, discuss any questions or difficulties in the Slack channel. You can also share challenging benchmarks that others can try to exercise their verifiers on.
Next week will be a normal lecture about Horn clauses and loop invariants.
|פורסם ב- 29/4/2021, 17:28:14 Created on 29/4/2021, 17:28:14 Создано 29/4/2021, 17:28:14 تم النشر ب- 29/4/2021, 17:28:14|
Lecture Today (April 27)
We will not have a lecture today.
The planned lecture on Horn Clauses will be given next week.
The course staff
|פורסם ב- 27/4/2021, 12:03:04 Created on 27/4/2021, 12:03:04 Создано 27/4/2021, 12:03:04 تم النشر ب- 27/4/2021, 12:03:04|
Instructions for Class on Tuesday
|(1) I remind you that the updated link for online attendance is located in the "Syllabus" tab (requires login).|
(2) Each team should prepare a *short* (5-10 mins) demo + presentation of the implementation. You don't need to prepare any slides, but if your system can generate a graphical visualization of the CFG it would be nice to show it.
(3) Send the instructors and email with a link to your source repository, GitHub or otherwise, so that we can refer to it throughout the semester.
See you on Tuesday.
|פורסם ב- 18/4/2021, 18:21:05 Created on 18/4/2021, 18:21:05 Создано 18/4/2021, 18:21:05 تم النشر ب- 18/4/2021, 18:21:05|
"@ensures" in sample programs
|On Tuesday, I showed a function `max3_v1` whose postcondition was written as an `@ensures` tag in the comment above the function definition.|
However, as you may well know, the parser discards all the comments.
While this was an unintentional oversight, let us make lemonade out of it: try to think of a way to change the program, such that the annotation is still accessible from the AST, and in a way that will allow your implementation to locate it. There is no single right answer -- you can do it however you like.
The semantics of `@ensures` is that the postcondition has to hold at *all exit points* from the function (`return` or end of body).
|עדכון אחרון ב- 9/4/2021, 14:37:05 Last updated on 9/4/2021, 14:37:05 Последняя модификация 9/4/2021, 14:37:05 تمت الحتلنة الأخيرة ب- 9/4/2021, 14:37:05|
Zoom link updated
|We have updated the link to the lectures to a more secure one -- token-protected and not publicly visible.|
Visit the "syllabus" tab on the course website to see the new link (requires login).
|עדכון אחרון ב- 6/4/2021, 23:20:45 Last updated on 6/4/2021, 23:20:45 Последняя модификация 6/4/2021, 23:20:45 تمت الحتلنة الأخيرة ب- 6/4/2021, 23:20:45|
Welcome and Survey
Welcome to Project in FV!
As you are all aware, lectures during this semester will be given in class as well as online.
To better prepare for the upcoming semester, please fill out this short questionnaire: https://forms.gle/RBfCepdLEb8atyFd6
Be sure that this information is not going to be used in any way. It is only meant for administrative preparations.
All the best, and see you soon!
|עדכון אחרון ב- 30/3/2021, 15:40:37 Last updated on 30/3/2021, 15:40:37 Последняя модификация 30/3/2021, 15:40:37 تمت الحتلنة الأخيرة ب- 30/3/2021, 15:40:37|