Formal Verification: EPFL Course (CS-550)
Fall 2020 Edition. Videos, Coursebook, Moodle, Discord
Construct 100% correct software! All project based.
Week 01: Introduction and Stainless
14.09.20 - 18.09.20
Lectures to watch: watch these videos (in alphabetical order):
Stainless Tutorials: 1 , 2 , 3 , 4
Labs to Do: Labs 01: Stainless
Week 02
Week 03
28.09.20 - 02.10.20
Videos:
Labs to Do: Labs 03: Amortized Queues in Coq (See how to install Coq and a short tutorial on Coq (video)).
Coq resources:
- Try Coq in browser: https://jscoq.github.io/
- Software Foundation Volume 1 - main text
Week 04
05.10.20 - 09.10.20
Videos:
Labs to Do: Labs 04: Relations and Transition Systems in Coq
Labs 04 solutions (extract the archive and run ./configure && make).
Week 05
12.10.20 - 16.10.20
Slides are here. Videos below:
Labs to Do: Discuss in group and with us your personalized lab.
Further overview videos to watch:
Prepare One-Page Proposal for Personalized Lab (1-page instructions for 1-page proposal will follow shortly)
Week 06
19.10.20 - 23.10.20
Lecture: Automating First-Order Logic Proofs Using Resolution (slides)
Labs to Do: Read the paper, record background paper presentations.
Deadline for both Labs 04 and for the One-Page Proposal
Instructions for Background Paper Presentations are available
Week 07
26.10.20 - 30.10.20
Videos:
Labs to Do: Read the paper, record background paper presentations.
Another round of meetings with staff about the project according to Doodle poll.
Week 08
02.11.20 - 06.11.20
Thursday, 5 November at 10am: deadline for recordings to be uploaded to tube.switch.ch
Labs to Do: Background presentations batch 1. We will play back your recorded presentations according to schedule and you will then answer questions from the audience including teaching staff.
Thursday
15:15 - 15:45: CafeSAT
Zilu Tian, Aaron Lippeveldts, Mikhail Makarov
15:45 - 16:15: SecChisel
Andra Bisca, Axel Marmet, Alexandre Pinazza
https://tube.switch.ch/videos/4225c2c2
SecChisel Framework for Security Verification of Secure Processor Architectures
16:15 - 16:45: Abstract Interpretation and Octagon Domain
Jérôme Boillot, Orégane Desrentes, Siang-Yun Lee, Dewmini Marakkalage
16:45 - 17:15: Purely Functional Priority Queue
Aurélien Debbas, Arthur Passuello, François Quellec, Michael Spierer
https://tube.switch.ch/videos/ca5949d3
Optimal Purely Functional Priority Queues
Friday
13:45 - 14:15: Combining WS1S and HOL
Zhendong Ang, Louis Vialar, Arthur Jacot, Simon Guilloud
Video: https://tube.switch.ch/videos/72f83c29
Paper: Combining WS1S and HOL
14:15 - 14:45: Concurrency and transactional memory in Dafny
Week 09
9.11.20 - 13.11.20
Thursday
15:15-15:45
Antoine Brunner, Baptiste Jacquemot, Yanick Paulo-Amaro: First-Order Theorem Proving and Vampire (live presentation)
15:45-16:15
Nicolas Rolin: Linear-Arithmetic Solver for DPLL(T) (video)
Friday
https://epfl.zoom.us/j/85473590280?pwd=ZTBjUnNMTXg4aW0rcCtGSDI1NGZWUT09
14:15-14:45
Samuel Chassot and Daniel Filipe Nunes Silva: Mechanizing the textbook proof of Huffman’s algorithm
Week 10
16.11.20 - 20.11.20
Videos:
Labs to Do: Work on your projects
Week 11
23.11.20 - 27.11.20
Labs to Do: Work on your projects
Week 12
30.11.20 - 04.12.20
Labs to Do: Work on your projects
Week 13
07.12.20 - 11.12.20
Labs to Do: Project presentations batch 1
Thursday
15:15 - 15:45: ZamSat
Zilu Tian, Aaron Lippeveldts, Mikhail Makarov
15:45 - 16:15: Formally Verified Chisel Designs
13:45 - 14:15: A Solver for WS1S
Louis Vialar, Arthur Jacot, Zhendong Ang, Simon Guilloud
14:15 - 14:45: Optimal Purely Functional Priority Queues
François Quellec, Arthur Passuello, Michael Spierer, Aurélien Debbas
Week 14
14.12.20 - 18.12.20
Labs to Do: Project presentation batch 2
Thursday
15:15 - 15:45: Concurrency and transactional memory in Dafny
Elisa Guerrant, Clément Burgelin, Hugo Hueber
15:45 - 16:15: First-Order Theorem Proving and Vampire
Antoine Brunner, Baptiste Jacquemot, Yanick Paulo-Amaro
16:15 - 16:45: Simplex
13:45 - 14:15: Abstract Interpretation and Octagon Domain
Jérôme Boillot, Orégane Desrentes, Siang-Yun Lee, Dewmini Marakkalage
14:15 - 14:45: Implementation and verification of encoder and decoder for prefix-free codes
Daniel Filipe Nunes Silva, Samuel Chassot
(Extended) Project reports and implementations are now due on 7 January 2021
General Information
Grading
GRADE will be computed based on projects:
- 40% Four labs to be done in groups, each group working independently on same projects:
- 10% Stainless Lab 1 - w1
- 10% Stainless Lab 2 - w2
- 10% Coq Lab 1 - w3
- 10% Coq Lab 2 - w4
- 60% Final project to be done in groups : you will choose a topic with our agreement
- 15% Presentation of a background paper (pre-recorded or streamed)
- 15% Results accomplished (how hard it was, how far you got)
- 15% Presentation of results (pre-recorded or streamed)
- 15% Final report
Staff
Instructors: Viktor Kuncak, Jad Hamza
PhD assistant: Romain Edelmann
Content
In this course we introduce formal verification as a principled approach for developing systems that do what they should do.
The course has two aspects:
- learning the practice of formal verification - how to use tools to construct verified software
- understanding the principles behind formal verification and the ways in which verification tools work
The course will have material related to 2019 edition but the grading will be based only on project work. Project can be a case study in developing a verified piece of software, an implementation of verification tool functionality, or a theoretical result about verification, constraint solving or theorem proving. Students present their projects with a written report as well as by recording a presentation of the background material and project results and answering our questions.
Lecture Format
Normally, our scheduled slot Thursday 15:15-17:00 in GR A3 30 will be for lectures, either pre-recorded or streamed from the lecture room and recorded. Even when there is a pre-recorded lecture for the week, an instructor will be present in the beginning of the lecture hour (in the scheduled lecture room) to answer your questions in person while maintaining the required distance.
Exercise and Lab Format
Because all of the grading is based on projects, exercises and labs serve the same purpose. Their goal is to help students do the projects.
Students will work in groups of 3 (or exceptionally 2 or 4) for all labs as well as for the final project. Groups will be formed at the start of the semester and will remain the same for the entirety of the semester.
Most of the interaction around projects with us will happen online because it is in practice not possible to maintain the distance while looking at another person's laptop screen. On the other hand, it is easy to share the screen and audio virtually.
There are two lab slots that we will support virtually, using Discord:
- Thursdays 17:15-19:00
- Fridays 13:15-15:00
Please join us on the following Discord server: https://discord.gg/UqXzZt6
In addition, in first few weeks a teaching staff member will be present in the beginning of the Friday slot from 13:00 in room CE1 103 to answer your questions in person.
If you need additional hours, please contact us using our EPFL contact pages to set up a virtual or physical meeting.
In the second part of the semester, there will be pre-recorded presentations by students doing projects, followed by questions and answers from the students and teaching staff.