EPFL videos and channels have moved to
mediaspace.epfl.ch
.
Find out more…
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
00-00, About the instructor (Viktor Kuncak)
0:55
01-01, What is Formal Verification?
10:22
50-01, Specification and Verification of a Blockchain Light Client
1:24:47
01-02, First Steps with Stainless
19:09
01-03, Auxiliary Assertions in Stainless
7:13
01-04, Unfolding recursive functions in Stainless
15:41
01-05, Disasters, Successes, and Inductive Invariants
36:56
02-01, Dispenser Example of Finite System
28:22
02-02, Finite Systems Expressed with Formulas
1:01:05
03-01, What is a Formal Proof?
35:41
03-02, Propositional Resolution
1:15:05
04-01, Simulation Relations
21:48
05-01, Presburger Arithmetic and Quantifier Elimination Introduction
51:27
05-02, Quantifier Elimination Steps for Presburger Arithmetic
42:17
06-01, Automating First-Order Logic Proofs Using Resolution
1:24:32
07-01, Converting Imperative Programs to Formulas
1:03:44
08-01, Hoare Logic, Strongest Postcondition, Weakest Precondition
27:09
01-01-Live1, Introduction to Formal Verification
28:15
01-02-Live2, Introduction to Stainless
25:08
01-03-Live3, Disasters, Successes, and Inductive Invariants
29:34
02-01-Live, Dispenser Example and its Stainless Representation
46:11
02-02-Live2, Finite Systems Expressed with Formulas
43:49
03-01-Live1, Checking invariants and bounded model checking. What is a formal proof?
1:08:55
03-02-Live2, Soundness and Completeness of a Propositional Proof System
46:50
03-02-Live3, Case Analysis Rule and Propositional Resolution, Live1
45:15
03-02-Live4, Propositional Resolution and SAT Solvers, Live2
45:54
05-01-Live1part, Introduction to Quantifier Elimination for Presburger Arithmetic
26:03
05-02-Live2, Quantifier Elimination Steps for Presburger Arithmetic
46:07
06-01-Live1, Automating First-Order Logic Proofs Using Resolution 1
46:57
06-02-Live2, Automating First-Order Logic Proofs Using Resolution 2
47:21
Previous
1 of 2
Next