LARA

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.

Moodle

Autumn 2019 Semester. 2h Lectures, 2h Exercises, 2h Labs. Continuous Control.

CS-550 in Course Catalog

Instructors: Viktor Kuncak, Jad Hamza, with the help of Romain Ruetschi

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.

Grading

  • 50% based on the quiz on 12 December
  • 50% 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 can be done in groups of 2-3 students. You will need to present the plan for the final lab in the last week of the semester.

Outline

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'

Thursday 15:15 Lecture 01: Introduction. Transition Systems: slides, Scala examples
Thursday 17:15 Labs 01: Scala, Stainless, and State Machines (Solutions)
Friday 13:15 Exercises 01: State machines and propositional logic (Solutions)

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)

Reading:

  • 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

Reading:

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:

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

Reading:

More advanced:


Part III: Automating Software Verification


Week 08, November 4

Week 09, November 11

Week 10, November 18

Thursday 15:15 Lecture 12: More QE. Satisfiability Modulo Theories and DPLL(T)
Thursday 17:15 Labs 06: SMT-based verifier for a language with integer state and recursion
Friday 13:15 More on SMT. Exercises: Quiz 2013, Quiz 2015

Milestones in SMT solver development:

Introduction from Selected VeriFun slides (Full VeriFun slides are here)


Future


Week 11, November 25

A web demo version of the Leon system:

Thursday 15:15 Lecture: Modelling simple state by translation. Modelling program heap. Intermediate verification languages (Boogie, Why3, Horn clauses, Inox)
Thursday 17:15 Personalized Labs
Friday 13:15 Lecture 14: Guest lecture by Nicolas Voirol on Stainless system architecture, encoding of recursion and higher-order functions

Part IV: Semantics for Verification


Week 12, December 2

Thursday 15:15 Lecture 13: Abstract Interpretation. Predicate Abstraction
Thursday 17:15 Personalized Labs
Friday 13:15 Exercises

Example paper: SideTrail: Verifying Time-Balancing of Cryptosystems (based on Boogie)

Week 13, December 9

Thursday 15:15 Quiz
Thursday 17:15 continue Quiz
Friday 13:15 Personalized Labs

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

  • 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

Background

Introduction

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