Formal verification

CS-550 / 6 credits

Language: English

Summary

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

Content

Topics may include (among others) some of the following:

Importance of Reliable Systems. Methodology of Formal Verification. Soundness and Completeness in Modeling and Tools. Successful Tools and Flagship Case Studies
Review of Sets, Relations, Computability, Propositional and First-Order Logic Syntax, Semantics, Sequent Calculus.
Completeness and Semi-Decidability for First-Order Logic. Inductive Definitions and Proof Trees. Higher-Order Logic and LCF Approach.
State Machines. Transition Formulas. Traces. Strongest Postconditions and Weakest Preconditions.
Hoare Logic. Inductive Invariants. Well-Founded Relations and Termination Measures
Linear Temporal Logic. System Verilog Assertions. Monitors
SAT Solvers and Bounded Model Checking
Model Checking using Binary Decision Diagrams
Loop Invariants. Hoare Logic. Statically Checked Function Contracts. Relational Semantics and Fixed-Point Semantics
Symbolic Execution. Satisfiability Modulo Theories
Abstract Interpretation
Set theory for verification

Learning Prerequisites

Recommended courses

CS-320 Computer language processing

Important concepts to start the course

Discrete Mathematics (e.g. Kenneth Rosen: Discrete Mathematics and Its Applications)

Learning Outcomes

By the end of the course, the student must be able to:

Formalize specifications
Synthesize loop invariants
Specify software functionality
Generalize inductive hypothesis
Critique current software development practices

Teaching methods

Instructors will present lectures and exercises and supervise labs on student laptops.

Expected student activities

Follow the course materials, take mid-term, and complete and explain projects during the semester.

Assessment methods

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.

Supervision

Office hours	Yes
Assistants	Yes
Forum	Yes

Resources

Bibliography

Harrison, J. (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge: Cambridge University Press. doi:10.1017/CBO9780511576430
Aaron Bradley and Zohar Manna: The Calculus of Computation - Decision Procedures with Applications to Verification, Springer 2007.
Michael Huth and Mark Rayan: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge University Press 2004.
Handbook of Model Checking, https://www.springer.com/de/book/9783319105741 Springer 2018. Including Chapter Model Checking Security Protocols by David Basin.
Tobias Nipkow, Gerwin Klein: Concrete Semantics with Isabelle/HOL. http://concrete-semantics.org/concrete-semantics.pdf
Nielson, Flemming, Nielson, Hanne R., Hankin, Chris: Principles of Program Analysis. ISBN 978-3-662-03811-6. Springer 1999.
Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory (To Truth Through Proof), Springer 2002.
http://logitext.mit.edu/tutorial

Ressources en bibliothèque

Notes/Handbook

https://lara.epfl.ch/w/fv

Websites

https://lara.epfl.ch/w/fv

Moodle Link

https://go.epfl.ch/CS-550

In the programs

Semester: Fall
Exam form: During the semester (winter session)
Subject examined: Formal verification
Lecture: 2 Hour(s) per week x 14 weeks
Exercises: 2 Hour(s) per week x 14 weeks
Project: 2 Hour(s) per week x 14 weeks
Type: optional

Semester: Fall
Exam form: During the semester (winter session)
Subject examined: Formal verification
Lecture: 2 Hour(s) per week x 14 weeks
Exercises: 2 Hour(s) per week x 14 weeks
Project: 2 Hour(s) per week x 14 weeks
Type: optional

Semester: Fall
Exam form: During the semester (winter session)
Subject examined: Formal verification
Lecture: 2 Hour(s) per week x 14 weeks
Exercises: 2 Hour(s) per week x 14 weeks
Project: 2 Hour(s) per week x 14 weeks
Type: optional

Semester: Fall
Exam form: During the semester (winter session)
Subject examined: Formal verification
Lecture: 2 Hour(s) per week x 14 weeks
Exercises: 2 Hour(s) per week x 14 weeks
Project: 2 Hour(s) per week x 14 weeks
Type: optional

Semester: Fall
Exam form: During the semester (winter session)
Subject examined: Formal verification
Lecture: 2 Hour(s) per week x 14 weeks
Exercises: 2 Hour(s) per week x 14 weeks
Project: 2 Hour(s) per week x 14 weeks
Type: optional

Semester: Fall
Exam form: During the semester (winter session)
Subject examined: Formal verification
Lecture: 2 Hour(s) per week x 14 weeks
Exercises: 2 Hour(s) per week x 14 weeks
Project: 2 Hour(s) per week x 14 weeks
Type: optional

Semester: Fall
Exam form: During the semester (winter session)
Subject examined: Formal verification
Lecture: 2 Hour(s) per week x 14 weeks
Exercises: 2 Hour(s) per week x 14 weeks
Project: 2 Hour(s) per week x 14 weeks
Type: optional

Semester: Fall
Exam form: During the semester (winter session)
Subject examined: Formal verification
Lecture: 2 Hour(s) per week x 14 weeks
Exercises: 2 Hour(s) per week x 14 weeks
Project: 2 Hour(s) per week x 14 weeks
Type: optional

Exam form: During the semester (winter session)
Subject examined: Formal verification
Lecture: 2 Hour(s) per week x 14 weeks
Exercises: 2 Hour(s) per week x 14 weeks
Project: 2 Hour(s) per week x 14 weeks
Type: optional

Semester: Fall
Exam form: During the semester (winter session)
Subject examined: Formal verification
Lecture: 2 Hour(s) per week x 14 weeks
Exercises: 2 Hour(s) per week x 14 weeks
Project: 2 Hour(s) per week x 14 weeks
Type: optional

Reference week

Légendes:

Lecture

Exercise, TP

Project, labs, other

Related courses

Results from graphsearch.epfl.ch.

	Mo	Tu	We	Th	Fr
8-9
9-10
10-11
11-12
12-13
13-14					INR219
14-15					INR219
15-16				GRA330
16-17				GRA330
17-18				GRA330
18-19				GRA330
19-20
20-21
21-22