Viktor Kuncak

70-05, Jimmy Koppel: Meta-metaprogramming 

30-09, Sequent Calculus with Equality

02-03, Idea of Symbolic Computation of Reachable States

70-01, Martingale-based Methods for Formal Verification and Certified Control of Stochastic Systems

60-02, Stainless Tutorial at ASPLOS 2022 Part 2

60-05, Stainless Verification System Tutorial by Viktor Kuncak and Jad Hamza, FMCAD 2021

70-03, Ondřej Lhoták: Taming Null References

70-04, Nadia Polikarpova: Synthesis of Safe Pointer-Manipulating Programs

30-08, Sequent Calculus

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

Total Functions: How and Why

Semantics and Verification of Concurrency

Jérôme Boillot: Abstract Interpretation in Stainless

Omega Continuity, Galois Connection, and AI Recipe

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

12-02-Live2, Lattices for Abstract Interpretation

12-01, Abstract Interpretation Idea

11-01-Live1, Introduction to SMT Solving

10-03, Recursion 2

10-02, Approximating Loops. Recursion 1

10-01, Loop Semantics Example

09-02, Relational Semantics of Loops

09-01, Monotonicity and Semantics of Local Variables

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

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

07-01-Live1, Converting Imperative Programs to Formulas

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

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

05-02-Live2, Quantifier Elimination Steps for Presburger Arithmetic

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