This is an old revision of the document!
Formal Verification EPFL Course (CS-550), Fall 2019
Autumn 2019 Semester. 2h Lectures, 2h Exercises, 2h Labs. Continuous Control
Instructors: Viktor Kuncak, Jad Hamza, with the help of Romain Edelmann, Georg Schmid, Romain Ruetschi
One of the verification tools used: Stainless
Introduction
In this course we introduce formal verification as a principled approach for developing systems that do what they should do.
Formal verification finds proofs that computer systems work under all scenarios of interest. Formal verification tools help developers construct such proofs, automatically searching for proofs using theorem proving and constraint solving (using, e.g. SMT solvers), and static analysis to discover program invariants. When it succeeds, formal verification is guaranteed to identify all software errors, including, for example, security vulnerabilities or cases when the computation produces a wrong numerical or symbolic result. The best approach to obtain formally verified software is to perform formal verification while software is developed, as opposed to after the fact.
Companies, research labs and research groups have developed proofs of correctness of operating system kernels, brake system for a metro line in Paris, compilers, databases, data structures, smartcard wallets, communication protocols, and distributed systems.
In this course we will learn how to use formal verification tools and explain the theory and the practice behind them.
Warmup videos by others:
Outline
First class: Thursday 19 September at 15:15 in the classroom INF213.
Part I: Introduction and Finite State Systems
Week 01, September 16
Thursday | 15:15 | Lecture 01: Introduction. State machines |
Thursday | 17:15 | Labs 01: Scala, Stainless, and State Machines |
Friday | 13:15 | Exercises 01: Proofs about state machines |
Week 02, September 23
Thursday | 15:15 | Lecture 02: Explicit-State Exploration. BDDs |
Thursday | 17:15 | Labs 02: Explicit-State Reachability Checker |
Friday | 13:15 | Exercises 02: BDDs |
Week 03, September 30
Thursday | 15:15 | Lecture 03: Bounded Model Checking and SAT |
Thursday | 17:15 | Labs 03: BDD-Based Reachability Checker |
Friday | 13:15 | Exercise 03: Propositional logic and SAT |
Week 04, October 7
Thursday | 15:15 | Lecture 04: Hardware Verification |
Thursday | 17:15 | Labs 04: SAT-Based Checker |
Friday | 13:15 | Lecture 05: Interpolation and Other Property-Based Algorithms |
Part II: Deductive Program Verification
Loop Invariants. Hoare Logic. Statically Checked Function Contracts. Relational Semantics and Fixed-Point Semantics. Symbolic Execution. Satisfiability Modulo Theories.
Part III: Abstract Interpretation
Abstract Interpretation framework. Predicate Abstraction.
Part IV: Proof Assistants and Verified Software
Stainless. Isabelle. Coq. Imperative programs with Heap. Concurrency.
Topic List
- 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
- Modeling Hardware: Verilog to Sequential Circuits
- 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 and Predicate Abstraction
- Information Flow and Taint Analysis
- Verification of Security Protocols
- Dependent and Refinement Types
Relevant Textbooks
- 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
- Aaron Bradley and Zohar Manna: The Calculus of Computation - Decision Procedures with Applications to Verification, Springer 2007.
- 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.
Background
- Kenneth H. Rosen. Discrete Mathematics and Its Applications. E.g. 8th Edition.
- Formally Verified Software in the Real World. Communications of the ACM, October 2018. https://cacm.acm.org/magazines/2018/10/231372-formally-verified-software-in-the-real-world/fulltext