LARA

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

Week 02

Week 03

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

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

https://tube.switch.ch/videos/6a168ea0

Paper: CafeSat: A Modern SAT Solver for Scala

15:45 - 16:15: SecChisel

16:15 - 16:45: Abstract Interpretation and Octagon Domain

Jérôme Boillot, Orégane Desrentes, Siang-Yun Lee, Dewmini Marakkalage

https://tube.switch.ch/videos/2bab8956

The octagon abstract domain

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

14:15-14:45

Samuel Chassot and Daniel Filipe Nunes Silva: Mechanizing the textbook proof of Huffman’s algorithm

Week 10

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

Week 14

14.12.20 - 18.12.20

Labs to Do: Project presentation batch 2

(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:

  1. learning the practice of formal verification - how to use tools to construct verified software
  2. 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.