Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
fv19:top [2019/08/21 13:46] vkuncak |
fv19:top [2019/08/21 15:04] vkuncak |
||
---|---|---|---|
Line 11: | Line 11: | ||
===== Introduction ===== | ===== Introduction ===== | ||
- | In this course we introduce formal verification as an approach for developing highly reliable systems. | + | 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 | Formal verification finds proofs that computer systems work | ||
Line 40: | Line 40: | ||
===== Outline ===== | ===== Outline ===== | ||
+ | **First class: Thursday 19 September at 15:15 in the classroom INF213.** | ||
+ | **Part I: Introduction and Finite State Systems** | ||
- | ===== Topics ===== | + | ==== 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 | Guest Lecture 03: Hardware Verification | | ||
+ | | Thursday | 17:15 | Labs 04: SAT-Based Checker | | ||
+ | | Friday | 13:15 | Interpolation-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 | * Importance of Reliable Systems. Methodology of Formal Verification. Soundness and Completeness in Modeling and Tools. Successful Tools and Flagship Case Studies |