Formal Verification: EPFL Course (CS-550), Fall 2019
In this course we introduce formal verification as a principled approach for developing systems that do what they should do.
Autumn 2019 Semester. 2h Lectures, 2h Exercises, 2h Labs. Continuous Control.
All project assignments will be in Scala. If you do not know Scala, please consider these free EPFL Courseware courses:
The primary verification tools used: Stainless. Stainless is a formal way of doing Scala.
- 40% based on the quiz on 12 December: 15:15-18:00. You can bring printed lecture and exercise slides
- 60% based on all lab assignments and home works taken together
There will be 7 labs in total: 6 fixed ones that everyone should do individually, and a 7th one that are to be done in groups of 1-3 students. You will need to present the plan for the final lab in the last week of the semester.
First class: Thursday 19 September at 15:15 in the classroom INF213.
The material consists of approximately four parts:
- I: Introduction and Finite State Systems
- II: Proof Assistants
- III: Automating Software Verification
- IV: Semantics for Verification
Part I: Introduction and Finite State Systems
Week 01, September 16
Watch and understand the Talk of J Moore 'Machines Reasoning about Machines'
Week 02, September 23
|Thursday||15:15||Lecture 02: Bounded Model Checking|
|Thursday||16:15||IC Colloquium by Catalin Hritcu, INRIA|
|Thursday||17:30||Labs 02: Bounded model checker (Solutions)|
|Friday||13:15||Exercises 02 (Solutions)|
- Chapter 10 of the Model Checking Handbook
Week 03, September 30
|Thursday||15:15||Lecture 03: Propositional Proofs and SAT Idea|
|Thursday||17:15||Continue Labs 02 (no new lab)|
|Friday||13:15||Lecture 04: SAT Solvers: Slides of Prof. Sharad Malik (Princeton), Further Slides|
- Chapter 9 of the Model Checking Handbook
- Chapter 24 and 2 of the Model Checking Handbook
Week 04, October 7
|Thursday||15:15||Lecture 05: Hardware Verification lecture by Barbara Jobstmann (see Moodle for slides)|
|Thursday||17:15||Labs 03: Building a SAT solver (Solutions)|
|Friday||13:15||Lecture 06: Linear Temporal Logic and Binary Decision Diagrams|
Week 05, October 14
|Thursday||15:15||Lecture 07: Interpolation-Based Model Checking,McMillan 2003 paper,Interpolant Strength|
|Thursday||17:15||Continue Labs 03|
|Friday||13:15||Exercises 03: Syntax, Semantics, and Exercises for First-Order Logic (Solutions)|
For further reading, check some of the recent papers:
Part II: Proof Assistants
Week 06, October 21
|Thursday||15:15||Lecture 08: LCF Approach to Formal Proof|
|Thursday||17:15||Labs 04: LCF Approach|
|Friday||13:15||Lecture 09: First-Order Logic Normal Forms and Resolution: Slide Deck 1, Slide Deck 2, check also material such as this|
Reading for LCF approach:
- Practical Logic and Automated Reasoning (Harrison), Chapter 6
Reading for resolution:
- Practical Logic and Automated Reasoning (Harrison), Chapter 3
Week 07, October 28
|Thursday||15:15||Lecture 10: Isabelle/HOL from Concrete Semantics with demos|
|Thursday||17:15||Continue Labs 04 and start Labs 05 on Isabelle|
|Friday||13:15||Quantifiers, Rules, and Structured Proofs, Sleepy Student Paradox Example|
- Concrete Semantics (source of the slides and demos)
Part III: Automating Software Verification
Week 08, November 4
|Thursday||15:15||Lecture 12: Hoare Logic and Translating Code to Formulas|
|Thursday||17:15||Labs 05 on Isabelle|
|Friday||13:15||Lecture 13: More on Hoare Logic|
Week 09, November 11
|Thursday||15:15||Lecture 14: Contexts, Local Variables, Loops|
|Thursday||17:15||Continue labs05 and do watch-and-answer Lab0-Rustan of talk of Rustan Leino 'Directions to and for Verified Software'|
|Friday||13:15||Lecture 15: Recursion. Quantifier Elimination|
Week 10, November 18
|Thursday||15:15||Lecture 16: More QE. Satisfiability Modulo Theories and DPLL(T)|
|Thursday||17:15||Labs 06: Verifier for Recursive Procedures|
|Friday||13:15||Lecture 17a: More on SMT. Exercises: Quiz 2013, Quiz 2015|
Milestones in SMT solver development:
- results of Nelson and Oppen, including Nelson's dissertation
- inclusion of SAT solvers and the DPLL(T) algorithm: Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)
- The SMT-LIB initiative with standardized format, benchmarks, and competitions
- The provers such as Z3 prover
Week 11, November 25
A web demo version of the Leon system:
Part IV: Semantics for Verification
Week 12, December 2
|Thursday||15:15||Lecture 19: Abstract Interpretation Introduction|
|Friday||13:15||Lecture 20: More Abstract Interpretation. Predicate Abstraction|
Week 13, December 9
|Thursday||15:15-18:00||Quiz in the usual INF room Quiz and Solutions|
|Friday||13:15||Personalized Labs: Final Choice of Topics by The end of Day|
Week 14, December 16
|Thursday||15:15||Personalized Labs Presentations|
|Thursday||17:15||Personalized Labs Presentations|
|Friday||13:15||Personalized Labs Presentations|
(Further) Topic List
- Modelling local state and program heap. Intermediate verification languages (Why3, Horn clauses, Inox)
- Example paper: SideTrail: Verifying Time-Balancing of Cryptosystems (based on Boogie)
- 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
- Aaron Bradley and Zohar Manna: The Calculus of Computation - Decision Procedures with Applications to Verification, Springer 2007.
- Handbook of Model Checking, https://www.springer.com/de/book/9783319105741 Springer 2018. Available online from within EPFL through the EPFL library
- Tobias Nipkow, Gerwin Klein: Concrete semantics with Isabelle/HOL. http://concrete-semantics.org/concrete-semantics.pdf
- John Harrison: Handbook of Practical Logic Logic and Automated Reasoning (resources)
- Michael Huth and Mark Rayan: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge University Press 2004.
- 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.
- 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
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.
A short illustrative video: What is Formal Verification? - by Galois, a formal methods company
Somewhat related past course: SAV 2017