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

Future Material

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
    • 10% Stainless Lab 2
    • 10% Coq Lab 1
    • 10% Coq Lab 2
  • 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) and 3-page summary
    • 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.