CS-550 Formal Verification

Viktor Kuncak, École polytechnique fédérale de Lausanne (EPFL)

7 September 2020, 65 videos, 5793 views

https://gitlab.epfl.ch/lara/cs550/

Viewable by everyone.

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

24 September 2021, 36 views

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

30 September 2021, 14 views

02-02-Live2, Finite Systems Expressed with Formulas

30 September 2021, 13 views

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

1 October 2021, 18 views

03-02-Live2, Soundness and Completeness of a Propositional Proof System

1 October 2021, 17 views

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

7 October 2021, 12 views

03-02-Live4, Propositional Resolution and SAT Solvers, Live2

7 October 2021, 12 views

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

8 October 2021, 17 views

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

8 October 2021, 14 views

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

16 October 2021, 8 views

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

16 October 2021, 9 views

07-01-Live1, Converting Imperative Programs to Formulas

21 October 2021, 8 views

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

21 October 2021, 19 views

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

22 October 2021, 97 views

09-01, Monotonicity and Semantics of Local Variables

28 October 2021, 95 views

09-02, Relational Semantics of Loops

28 October 2021, 75 views

10-01, Loop Semantics Example

29 October 2021, 64 views

10-02, Approximating Loops. Recursion 1

29 October 2021, 22 views

10-03, Recursion 2

29 October 2021, 19 views

11-01-Live1, Introduction to SMT Solving

4 November 2021, 23 views

12-01, Abstract Interpretation Idea

11 November 2021, 44 views

12-02-Live2, Lattices for Abstract Interpretation

11 November 2021, 37 views

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

18 November 2021, 23 views

Omega Continuity, Galois Connection, and AI Recipe

18 November 2021, 26 views

Jérôme Boillot: Abstract Interpretation in Stainless

22 November 2021, 19 views

Load more…