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
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.
Warmup videos by others:
Topics
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