EPFL
EN
DE
Channels
Search
Sign in
Viktor Kuncak
École polytechnique fédérale de Lausanne (EPFL)
Thumbnails
List
Recent
Most recent on top
Oldest
Oldest on top
A-Z
Alphabetically
60-02, Stainless Tutorial at ASPLOS 2022 Part 2
1:15:30
Stainless Verification System Tutorial by Viktor Kuncak and Jad Hamza, FMCAD 2021
1:13:11
Ondřej Lhoták: Taming Null References
1:16:48
Synthesis of Safe Pointer-Manipulating Programs
1:11:56
Sequent Calculus
44:50
An Introduction to Iris: Higher-Order Concurrent Separation Logic
51:36
Total Functions: How and Why
47:35
Semantics and Verification of Concurrency
43:58
Jérôme Boillot: Abstract Interpretation in Stainless
43:32
Omega Continuity, Galois Connection, and AI Recipe
45:53
13-01-Live1, From Lattice Products to Tarski's Fixedpoint Theorem
34:42
12-02-Live2, Lattices for Abstract Interpretation
43:03
12-01, Abstract Interpretation Idea
41:43
11-01-Live1, Introduction to SMT Solving
30:08
10-03, Recursion 2
40:20
10-02, Approximating Loops. Recursion 1
10:25
10-01, Loop Semantics Example
15:16
09-02, Relational Semantics of Loops
44:22
09-01, Monotonicity and Semantics of Local Variables
45:12
07-03-Live3, Hoare Logic, Strongest Postcondition, Weakest Precondition Part 2
26:16
07-02-Live2, Hoare Logic, Strongest Postcondition, Weakest Precondition Part 1
46:42
07-01-Live1, Converting Imperative Programs to Formulas
37:20
06-02-Live2, Automating First-Order Logic Proofs Using Resolution 2
47:21
06-01-Live1, Automating First-Order Logic Proofs Using Resolution 1
46:57
05-02-Live2, Quantifier Elimination Steps for Presburger Arithmetic
46:07
05-01-Live1part, Introduction to Quantifier Elimination for Presburger Arithmetic
26:03
03-02-Live4, Propositional Resolution and SAT Solvers, Live2
45:54
03-02-Live3, Case Analysis Rule and Propositional Resolution, Live1
45:15
03-02-Live2, Soundness and Completeness of a Propositional Proof System
46:50
03-01-Live1, Checking invariants and bounded model checking. What is a formal proof?
1:08:55
Previous
1 of 2
Next
