Viktor Kuncak

00-00, About the instructor (Viktor Kuncak)

12-01, Abstract Interpretation Idea

10-02, Approximating Loops. Recursion 1

06-01, Automating First-Order Logic Proofs Using Resolution

06-01-Live1, Automating First-Order Logic Proofs Using Resolution 1

06-02-Live2, Automating First-Order Logic Proofs Using Resolution 2

01-03, Auxiliary Assertions in Stainless

03-02-Live3, Case Analysis Rule and Propositional Resolution, Live1

03-01-Live1, Checking invariants and bounded model checking. What is a formal proof?

07-01, Converting Imperative Programs to Formulas

07-01-Live1, Converting Imperative Programs to Formulas

01-05, Disasters, Successes, and Inductive Invariants

01-03-Live3, Disasters, Successes, and Inductive Invariants

02-01-Live, Dispenser Example and its Stainless Representation

02-01, Dispenser Example of Finite System

02-02-Live2, Finite Systems Expressed with Formulas

02-02, Finite Systems Expressed with Formulas

01-02, First Steps with Stainless

13-01-Live1, From Lattice Products to Tarski's Fixedpoint Theorem

08-01, Hoare Logic, Strongest Postcondition, Weakest Precondition

07-02-Live2, Hoare Logic, Strongest Postcondition, Weakest Precondition Part 1

07-03-Live3, Hoare Logic, Strongest Postcondition, Weakest Precondition Part 2

02-03, Idea of Symbolic Computation of Reachable States

01-01-Live1, Introduction to Formal Verification

05-01-Live1part, Introduction to Quantifier Elimination for Presburger Arithmetic

11-01-Live1, Introduction to SMT Solving

01-02-Live2, Introduction to Stainless

Jérôme Boillot: Abstract Interpretation in Stainless

70-05, Jimmy Koppel: Meta-metaprogramming 

70-02, Lars Birkedal: An Introduction to Iris, Higher-Order Concurrent Separation Logic