Skip to content

Latest commit

 

History

History
104 lines (82 loc) · 7.86 KB

README.md

File metadata and controls

104 lines (82 loc) · 7.86 KB

EPFL CS550 - Formal Verification

Moodle, Coursebook

This repository is the homepage of the course Formal Verification and hosts the material necesary for the labs.

Staff:

Grading

The grade is based on the written mid-term, as well as code, documentation, and explanation of projects during the semester. Specific percentages will be communicated in the first class and posted here.

The types of graded materials will include:

  • 40% Late mid-term written exam in November (see this folder with past exams)
  • 20% total: four-five labs, to be done in groups, each group working independently on same projects
  • 40% final project to be done in groups, you will choose a topic with our agreement
    • 10% Written presentation of a background paper
    • 10% Results accomplished (how hard it was, how far you got)
    • 10% Presentation of results
    • 10% Final report

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 follow a similar structure to the 2023 edition. 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 a live presentation of project results, answering our questions.

Note that slides can be found underneath each lecture video on switch tube linkes below.

Books

In the reading list below, HandAR-Ch.2 means Chapter 2 in the Handbook of Practical Logic and Automated Reasoning Above, whereas HandMC-Ch.9 means Chapter 9 of the Handbook of Model Checking, etc.

NOTE

To see the material, please visit https://mediaspace.epfl.ch , log in with your EPFL credentials and select this channel. Slides and listings are attached underneath the videos.

COURSE OUTLINE

Week Day Date Time Room Topic Videos & Slides
1 Thu 12.09.2024 15:15 GRA330 Lecture 1 Intro to FV, Intro to Stainless, Auxiliary Assertions, Unfolding, Disasters, Successes, and Inductive Invariants
17:15 GRA330 Lecture 2 Dispenser Example, Finite Systems Expressed with Formulas
Reading: HandMC-Ch.10
Follow: Stainless Tutorial Videos and materials
Fri 13.09.2024 13:15 INR219 Lecture 3 What is a Formal Proof? and Propositional Resolution
2 Thu 19.09.2024 15:15 GRA330 Lecture 2 continue Propositional Resolution
17:15 GRA330 Lab 1
Fri 20.09.2024 13:15 INR219 Exercises 1 Propositional Logic
Thu 26.09.2024 15:15 GRA330
17:15 GRA330 Lab 2 A communication protocol in Stainless
Fri 27.09.2024 13:15 INR219 Exercises 2 Traces, SAT, models
Thu 03.10.2024 15:15 GRA330
17:15 GRA330
Fri 04.10.2024 13:15 INR219
Thu 10.10.2024 15:15 GRA330
17:15 GRA330
Fri 11.10.2024 13:15 INR219
Thu 17.10.2024 15:15 GRA330
17:15 GRA330
Fri 18.10.2024 13:15 INR219
Thu 24.10.2024 15:15 Holidays
17:15 Holidays
Fri 25.10.2024 13:15 Holidays
Thu 31.10.2024 15:15 GRA330
17:15 GRA330
Fri 01.11.2024 13:15 INR219
Thu 07.11.2024 15:15 GRA330
17:15 GRA330
Fri 08.11.2024 13:15 INR219
Thu 14.11.2024 15:15 GRA330
17:15 GRA330
Fri 15.11.2024 13:15 INR219
Thu 21.11.2024 15:15 GRA330
17:15 GRA330
Fri 22.11.2024 13:15 INR219
Thu 28.11.2024 15:15 GRA330, AAC114 Midterm, until 18:00
Fri 29.11.2024 13:15 INR219
Thu 05.12.2024 15:15 GRA330
17:15 GRA330
Fri 06.12.2024 13:15 INR219
Thu 12.12.2024 15:15 GRA330
17:15 GRA330
Fri 13.12.2024 13:15 INR219
Thu 19.12.2024 15:15 GRA330
17:15 GRA330
Fri 20.12.2024 13:15 INR219

Midterm exam: Thursday, 28 November, 15:00-18:00