Formal verification
CS-550
Media
CS-550 Formal Verification
[CS214 W13 FP] Formal Verification (2024-12-09)
09.12.2024, 21:48
Andrew J Reynolds: Proofs in cvc5
09.07.2024, 16:47
More information: https://homepage.cs.uiowa.edu/~ajreynol/
Julian Parsert: Guiding Function Synthesis with AI
23.06.2024, 21:50
Mathias Fleury and Bruno Andreotti: Alethe, A flexible proof format with fine-grained steps
23.06.2024, 21:34
Geoff Sutcliffe: The TPTP formats for Proofs and Models
23.06.2024, 21:14
Carsten Fuhs: Proving Equivalence of Imperative Programs via Constrained Rewriting Induction
23.06.2024, 20:37
Philipp Rümmer: On Regular Constraint Propagation for Solving String Constraints
23.06.2024, 18:16
Jasmin Blanchette: Formalizing Saturation, Resolution, and Superposition in Isabelle/HOL
22.06.2024, 23:35
Chelsea Edmonds: Probabilistic Methods for Combinatorial Structures in Isabelle/HOL
22.06.2024, 23:15
John Harrison: Theorem Proving Infrastructure for Verified Cryptography
21.06.2024, 18:02
Shankar: Beautiful Formalizations And Proofs
21.06.2024, 17:48
[PS2024] Jeremy Avigad: Mathematical Structures in Dependent Type Theory
21.06.2024, 17:22
06-03 Term Models for First-Order Logic
12.10.2023, 17:38
Niki Vazou: Practicality and Soundness of Refinement Types
28.09.2023, 16:08
Refinement types decorate the types of a programming language with logical predicates to allow rnore expressive type specifications. Originally, refinement type based specifications were restricted to SMT decidable theories arnd allowed automatic "light" verification, for example properties like non-division by zero or in-bound indexing. Verification of such light properties though requires "deeper" specifications, for example "is append associative?" or even "does your language preserve typing?" In this talk, I will present an overview of Liquid Haskell's refinement types and discuss if they are practical, general, expressive, and sound.
Niki Vazou is an associate research professor at IMDEA Software Institute. She works on verification of functional programming and the foundations and applications of refinement types. Niki did her PhD at uc San Diego where she developed liquid Haskell. She has received the Microsoft Research Fellowship and the ERC Starting Grant.
70-05, Jimmy Koppel: Meta-metaprogramming
20.11.2022, 19:53
Programming languages researchers have developed many advanced tools that promise to greatly ease software engineering. Yet even conceptually simple tools are expensive to implement fully due to the complexity of the target language, and standard techniques tie an implementation to a particular target language. In order to make the development of advanced programming tools economical, these problems demand new techniques for decomposing the development of tools and automating portions of their construction, which I collectively dub “meta-metaprogramming."
In this talk, I will present my work on new techniques and frameworks for making tools easier to build and more general, and tools built on them. First I will present Cubix, a "One Tool, Many Languages" framework that allows a single tool to quickly be written for multiple programming languages. We have used Cubix to build Yogo, a semantic search tool capable of finding equivalent patterns in C, Java, and Python from a single shared query. Second, I will present Mandate, the world's first control-flow graph generator generator, able to generate multiple varieties of CFG-generator given a programming language's formal semantics. Finally, I will present our ongoing work on ECTAs (equality-constrained tree automata), a new type of data structure/constraint-solver able to efficiently search large spaces of programs subject to certain constraints. We have used ECTAs to build two synthesizers for Haskell, Hectare and Spectacular, which solidly beat their pre-existing competitors (Hoogle+ and QuickSpec) with only a fraction the engineering-effort.
30-09, Sequent Calculus with Equality
28.10.2022, 22:17
02-03, Idea of Symbolic Computation of Reachable States
07.10.2022, 23:34
70-01, Martingale-based Methods for Formal Verification and Certified Control of Stochastic Systems
09.08.2022, 16:27
60-04, Stainless Tutorial at ASPLOS 2022 Part 4
05.03.2022, 11:25
60-03, Stainless Tutorial at ASPLOS 2022 Part 3
05.03.2022, 11:24
60-01, Stainless Tutorial at ASPLOS 2022 Part 1
05.03.2022, 11:23
60-02, Stainless Tutorial at ASPLOS 2022 Part 2
01.03.2022, 13:11
60-05, Stainless Verification System Tutorial by Viktor Kuncak and Jad Hamza, FMCAD 2021
28.02.2022, 10:57
Stainless ( https://stainless.epfl.ch ) is an open-source tool for verifying and finding errors in programs written in the Scala programming language. This tutorial will not assume any knowledge of Scala. It aims to get first-time users started with verification tasks by introducing the language, providing modelling and verification tips, and giving a glimpse of the tool's inner workings (encoding into functional programs, function unfolding, and using theories of satisfiability modulo theory solvers Z3 and CVC4).
Stainless (and its predecessor, Leon) has been developed primarily in the EPFL's Laboratory for Automated Reasoning and Analysis in the period from 2011-2021. Its core specification and implementation language are typed recursive higher-order functional programs (imperative programs are also supported by automated translation to their functional semantics). Stainless can verify that functions are correct for all inputs with respect to provided preconditions and postconditions, it can prove that functions terminate (with optionally provided termination measure functions), and it can provide counter-examples to safety properties. Stainless enables users to write code that is both executed and verified using the same source files. Users can compile programs using the Scala compiler and run them on the JVM. For programs that adhere to certain discipline, users can generate source code in a small fragment of C and then use standard C compilers.
https://github.com/epfl-lara/fmcad2021tutorial
70-03, Ondřej Lhoták: Taming Null References
07.12.2021, 23:46
Abstract
Null references have been called the Billion Dollar Mistake in programming language design for all the errors, crashes, and vulnerabilities that they have caused over several decades. If null references are so bad, why do popular programming languages still promote their use? Do they have essential use cases?
I will report on our efforts to eliminate the disadvantages of null references while keeping support for existing programming idioms.
Our implementation is in the Scala language, but our conclusions can also help designers of other new programming languages.
Most uses of null references can be classified as either implementing optional values or initializing groups of related objects. For the former use case, practical alternatives exist, so the main challenge is retaining compatibility with existing codebases. The latter use case requires more fundamental changes in language design, type systems, and static analysis to ensure safety while still allowing widely used data structures and initialization patterns.
About the Speaker
Ondřej Lhoták is an Associate Professor at the University of Waterloo and a Visiting Professor in the LAMP group at EPFL until June 2022. His research interests are in static reasoning about the behaviour of programs in object-oriented programming languages, with a particular focus on Scala.
70-04, Nadia Polikarpova: Synthesis of Safe Pointer-Manipulating Programs
07.12.2021, 22:28
Abstract
Low-level pointer-manipulating programs form the backbone of our digital infrastructure. Unfortunately, they are susceptible to memory safety bugs, such as buffer overflows and use-after-free, which lead to crashes and security vulnerabilities. A promising approach to eliminating memory safety bugs is to use
program synthesis technology to generate provably safe low-level code automatically from high-level specifications.
In this talk I will present a program synthesizer SuSLik, which accepts a logical specification as input, and produces a provably safe C program as output. SuSLik is the first synthesizer capable of generating a wide range of operations on linked data structures (such as singly- and doubly-linked lists, sorted lists, and trees) without additional hints from the user. To make this possible, SuSLik relies on a novel proof system—synthetic separation logic—to derive correct-by-construction programs directly from their specifications.
About the Speaker
Nadia Polikarpova is an assistant professor at UC San Diego, and a member of the Programming Systems group. She received her Ph.D. in Computer Science from ETH Zurich in 2014, and then spent a couple years as a postdoctoral researcher at MIT. Nadia's research interests are in program synthesis, program verification, and type systems. She is a 2020 Sloan Fellow, and a recipient of the 2020 NSF Career Award and the 2020 Intel Rising Stars Award.
30-08, Sequent Calculus
02.12.2021, 17:26
70-02, Lars Birkedal: An Introduction to Iris, Higher-Order Concurrent Separation Logic
29.11.2021, 20:51
Abstract
Modern programming languages such as Scala, Java, and Rust are examples of concurrent higher-order imperative programming languages.
In this talk I will introduce our research on Iris, a logical framework, implemented and verified in the Coq proof assistant, which can be used for mathematical reasoning about safety and correctness of concurrent higher-order imperative programs. (See iris-project.org for more about Iris.)
Bio
Lars Birkedal is Professor of Computer Science at Aarhus University. He received his Ph.D. in Computer Science from Carnegie Mellon University, USA, in Dec. 1999 and until Dec. 2012 he was at the IT University of Copenhagen, Denmark. He served as Head of Department of Computer Science in Aarhus from 2014 to 2017.
Lars Birkedal is a Fellow of the ACM, an elected member of the Royal Danish Academy of Sciences and Letters, the recipient of a Villum Investigator grant from the Villum Foundation 2019, the Danish Minister of Research Elite Research Award 2015, and the ACM SIGPLAN Milner Award 2013. Lars Birkedal’s main research interests lie in the area of logic and semantics of programming languages and type theories. Current work focuses on program logics for reasoning about concurrent, higher-order, and imperative programs; cyber-security; and type theories with guarded recursion.
Host: Martin Odersky and Viktor Kuncak
Total Functions: How and Why
26.11.2021, 22:22
Semantics and Verification of Concurrency
26.11.2021, 12:07
Jérôme Boillot: Abstract Interpretation in Stainless
22.11.2021, 17:21
Omega Continuity, Galois Connection, and AI Recipe
18.11.2021, 18:30
13-01-Live1, From Lattice Products to Tarski's Fixedpoint Theorem
18.11.2021, 18:27
12-02-Live2, Lattices for Abstract Interpretation
11.11.2021, 21:37
12-01, Abstract Interpretation Idea
11.11.2021, 21:31
11-01-Live1, Introduction to SMT Solving
04.11.2021, 21:07
10-03, Recursion 2
29.10.2021, 17:05
10-02, Approximating Loops. Recursion 1
29.10.2021, 17:04
10-01, Loop Semantics Example
29.10.2021, 17:01
09-02, Relational Semantics of Loops
28.10.2021, 17:22
09-01, Monotonicity and Semantics of Local Variables
28.10.2021, 17:18
07-03-Live3, Hoare Logic, Strongest Postcondition, Weakest Precondition Part 2
22.10.2021, 21:29
07-02-Live2, Hoare Logic, Strongest Postcondition, Weakest Precondition Part 1
21.10.2021, 22:52
07-01-Live1, Converting Imperative Programs to Formulas
21.10.2021, 22:50
06-02-Live2, Automating First-Order Logic Proofs Using Resolution 2
16.10.2021, 23:21
06-01-Live1, Automating First-Order Logic Proofs Using Resolution 1
16.10.2021, 23:20
05-02-Live2, Quantifier Elimination Steps for Presburger Arithmetic
08.10.2021, 23:12
05-01-Live1part, Introduction to Quantifier Elimination for Presburger Arithmetic
08.10.2021, 23:10
03-02-Live4, Propositional Resolution and SAT Solvers, Live2
07.10.2021, 23:57
03-02-Live3, Case Analysis Rule and Propositional Resolution, Live1
07.10.2021, 23:55
03-02-Live2, Soundness and Completeness of a Propositional Proof System
01.10.2021, 22:54
03-01-Live1, Checking invariants and bounded model checking. What is a formal proof?
01.10.2021, 22:48
02-02-Live2, Finite Systems Expressed with Formulas
30.09.2021, 22:46
02-01-Live, Dispenser Example and its Stainless Representation
30.09.2021, 22:44
01-03-Live3, Disasters, Successes, and Inductive Invariants
24.09.2021, 12:30
01-02-Live2, Introduction to Stainless
24.09.2021, 12:26
01-01-Live1, Introduction to Formal Verification
24.09.2021, 12:14
Live recording of lecture 01 of Formal Verification EPFL course, as given on 2021-09-23 from 15:15-16:45.
08-01, Hoare Logic, Strongest Postcondition, Weakest Precondition
19.11.2020, 00:50
07-01, Converting Imperative Programs to Formulas
28.10.2020, 23:29
06-01, Automating First-Order Logic Proofs Using Resolution
22.10.2020, 16:37
05-02, Quantifier Elimination Steps for Presburger Arithmetic
15.10.2020, 00:20
05-01, Presburger Arithmetic and Quantifier Elimination Introduction
14.10.2020, 21:28
04-01, Simulation Relations
08.10.2020, 17:09
03-20, Short Coq Tutorial
02.10.2020, 14:46
Recording of the Coq tutorial presented on Friday 02/10/20.
03-02, Propositional Resolution
01.10.2020, 03:48
03-01, What is a Formal Proof?
30.09.2020, 19:30
02-02, Finite Systems Expressed with Formulas
24.09.2020, 02:33
02-01, Dispenser Example of Finite System
24.09.2020, 01:29
01-05, Disasters, Successes, and Inductive Invariants
17.09.2020, 04:03
01-04, Unfolding recursive functions in Stainless
17.09.2020, 02:04
01-03, Auxiliary Assertions in Stainless
16.09.2020, 22:12
01-02, First Steps with Stainless
13.09.2020, 00:22
50-01, Specification and Verification of a Blockchain Light Client
11.09.2020, 16:32
00-01, About the instructor (Jad Hamza)
10.09.2020, 11:55
01-21, Stainless Tutorial 1/4
09.09.2020, 11:17
https://github.com/epfl-lara/stainless/releases
Important: you must have Java 8 installed (other versions of Java might make Stainless crash)
01-01, What is Formal Verification?
09.09.2020, 11:15
00-00, About the instructor (Viktor Kuncak)
08.09.2020, 10:42
Viktor Kuncak (http://lara.epfl.ch/~kuncak/) is an associate professor (with tenure) in the School of Computer and Communication sciences of EPFL (Ecole Polytechnique Federale de Lausanne). He joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.
Media
CS-550 Formal Verification
[CS214 W13 FP] Formal Verification (2024-12-09)
09.12.2024, 21:48
Andrew J Reynolds: Proofs in cvc5
09.07.2024, 16:47
More information: https://homepage.cs.uiowa.edu/~ajreynol/
Julian Parsert: Guiding Function Synthesis with AI
23.06.2024, 21:50
Mathias Fleury and Bruno Andreotti: Alethe, A flexible proof format with fine-grained steps
23.06.2024, 21:34
Geoff Sutcliffe: The TPTP formats for Proofs and Models
23.06.2024, 21:14
Carsten Fuhs: Proving Equivalence of Imperative Programs via Constrained Rewriting Induction
23.06.2024, 20:37
Philipp Rümmer: On Regular Constraint Propagation for Solving String Constraints
23.06.2024, 18:16
Jasmin Blanchette: Formalizing Saturation, Resolution, and Superposition in Isabelle/HOL
22.06.2024, 23:35
Chelsea Edmonds: Probabilistic Methods for Combinatorial Structures in Isabelle/HOL
22.06.2024, 23:15
John Harrison: Theorem Proving Infrastructure for Verified Cryptography
21.06.2024, 18:02
Shankar: Beautiful Formalizations And Proofs
21.06.2024, 17:48
[PS2024] Jeremy Avigad: Mathematical Structures in Dependent Type Theory
21.06.2024, 17:22
06-03 Term Models for First-Order Logic
12.10.2023, 17:38
Niki Vazou: Practicality and Soundness of Refinement Types
28.09.2023, 16:08
Refinement types decorate the types of a programming language with logical predicates to allow rnore expressive type specifications. Originally, refinement type based specifications were restricted to SMT decidable theories arnd allowed automatic "light" verification, for example properties like non-division by zero or in-bound indexing. Verification of such light properties though requires "deeper" specifications, for example "is append associative?" or even "does your language preserve typing?" In this talk, I will present an overview of Liquid Haskell's refinement types and discuss if they are practical, general, expressive, and sound.
Niki Vazou is an associate research professor at IMDEA Software Institute. She works on verification of functional programming and the foundations and applications of refinement types. Niki did her PhD at uc San Diego where she developed liquid Haskell. She has received the Microsoft Research Fellowship and the ERC Starting Grant.
70-05, Jimmy Koppel: Meta-metaprogramming
20.11.2022, 19:53
Programming languages researchers have developed many advanced tools that promise to greatly ease software engineering. Yet even conceptually simple tools are expensive to implement fully due to the complexity of the target language, and standard techniques tie an implementation to a particular target language. In order to make the development of advanced programming tools economical, these problems demand new techniques for decomposing the development of tools and automating portions of their construction, which I collectively dub “meta-metaprogramming."
In this talk, I will present my work on new techniques and frameworks for making tools easier to build and more general, and tools built on them. First I will present Cubix, a "One Tool, Many Languages" framework that allows a single tool to quickly be written for multiple programming languages. We have used Cubix to build Yogo, a semantic search tool capable of finding equivalent patterns in C, Java, and Python from a single shared query. Second, I will present Mandate, the world's first control-flow graph generator generator, able to generate multiple varieties of CFG-generator given a programming language's formal semantics. Finally, I will present our ongoing work on ECTAs (equality-constrained tree automata), a new type of data structure/constraint-solver able to efficiently search large spaces of programs subject to certain constraints. We have used ECTAs to build two synthesizers for Haskell, Hectare and Spectacular, which solidly beat their pre-existing competitors (Hoogle+ and QuickSpec) with only a fraction the engineering-effort.
30-09, Sequent Calculus with Equality
28.10.2022, 22:17
02-03, Idea of Symbolic Computation of Reachable States
07.10.2022, 23:34
70-01, Martingale-based Methods for Formal Verification and Certified Control of Stochastic Systems
09.08.2022, 16:27
60-04, Stainless Tutorial at ASPLOS 2022 Part 4
05.03.2022, 11:25
60-03, Stainless Tutorial at ASPLOS 2022 Part 3
05.03.2022, 11:24
60-01, Stainless Tutorial at ASPLOS 2022 Part 1
05.03.2022, 11:23
60-02, Stainless Tutorial at ASPLOS 2022 Part 2
01.03.2022, 13:11
60-05, Stainless Verification System Tutorial by Viktor Kuncak and Jad Hamza, FMCAD 2021
28.02.2022, 10:57
Stainless ( https://stainless.epfl.ch ) is an open-source tool for verifying and finding errors in programs written in the Scala programming language. This tutorial will not assume any knowledge of Scala. It aims to get first-time users started with verification tasks by introducing the language, providing modelling and verification tips, and giving a glimpse of the tool's inner workings (encoding into functional programs, function unfolding, and using theories of satisfiability modulo theory solvers Z3 and CVC4).
Stainless (and its predecessor, Leon) has been developed primarily in the EPFL's Laboratory for Automated Reasoning and Analysis in the period from 2011-2021. Its core specification and implementation language are typed recursive higher-order functional programs (imperative programs are also supported by automated translation to their functional semantics). Stainless can verify that functions are correct for all inputs with respect to provided preconditions and postconditions, it can prove that functions terminate (with optionally provided termination measure functions), and it can provide counter-examples to safety properties. Stainless enables users to write code that is both executed and verified using the same source files. Users can compile programs using the Scala compiler and run them on the JVM. For programs that adhere to certain discipline, users can generate source code in a small fragment of C and then use standard C compilers.
https://github.com/epfl-lara/fmcad2021tutorial
70-03, Ondřej Lhoták: Taming Null References
07.12.2021, 23:46
Abstract
Null references have been called the Billion Dollar Mistake in programming language design for all the errors, crashes, and vulnerabilities that they have caused over several decades. If null references are so bad, why do popular programming languages still promote their use? Do they have essential use cases?
I will report on our efforts to eliminate the disadvantages of null references while keeping support for existing programming idioms.
Our implementation is in the Scala language, but our conclusions can also help designers of other new programming languages.
Most uses of null references can be classified as either implementing optional values or initializing groups of related objects. For the former use case, practical alternatives exist, so the main challenge is retaining compatibility with existing codebases. The latter use case requires more fundamental changes in language design, type systems, and static analysis to ensure safety while still allowing widely used data structures and initialization patterns.
About the Speaker
Ondřej Lhoták is an Associate Professor at the University of Waterloo and a Visiting Professor in the LAMP group at EPFL until June 2022. His research interests are in static reasoning about the behaviour of programs in object-oriented programming languages, with a particular focus on Scala.
70-04, Nadia Polikarpova: Synthesis of Safe Pointer-Manipulating Programs
07.12.2021, 22:28
Abstract
Low-level pointer-manipulating programs form the backbone of our digital infrastructure. Unfortunately, they are susceptible to memory safety bugs, such as buffer overflows and use-after-free, which lead to crashes and security vulnerabilities. A promising approach to eliminating memory safety bugs is to use
program synthesis technology to generate provably safe low-level code automatically from high-level specifications.
In this talk I will present a program synthesizer SuSLik, which accepts a logical specification as input, and produces a provably safe C program as output. SuSLik is the first synthesizer capable of generating a wide range of operations on linked data structures (such as singly- and doubly-linked lists, sorted lists, and trees) without additional hints from the user. To make this possible, SuSLik relies on a novel proof system—synthetic separation logic—to derive correct-by-construction programs directly from their specifications.
About the Speaker
Nadia Polikarpova is an assistant professor at UC San Diego, and a member of the Programming Systems group. She received her Ph.D. in Computer Science from ETH Zurich in 2014, and then spent a couple years as a postdoctoral researcher at MIT. Nadia's research interests are in program synthesis, program verification, and type systems. She is a 2020 Sloan Fellow, and a recipient of the 2020 NSF Career Award and the 2020 Intel Rising Stars Award.
30-08, Sequent Calculus
02.12.2021, 17:26
70-02, Lars Birkedal: An Introduction to Iris, Higher-Order Concurrent Separation Logic
29.11.2021, 20:51
Abstract
Modern programming languages such as Scala, Java, and Rust are examples of concurrent higher-order imperative programming languages.
In this talk I will introduce our research on Iris, a logical framework, implemented and verified in the Coq proof assistant, which can be used for mathematical reasoning about safety and correctness of concurrent higher-order imperative programs. (See iris-project.org for more about Iris.)
Bio
Lars Birkedal is Professor of Computer Science at Aarhus University. He received his Ph.D. in Computer Science from Carnegie Mellon University, USA, in Dec. 1999 and until Dec. 2012 he was at the IT University of Copenhagen, Denmark. He served as Head of Department of Computer Science in Aarhus from 2014 to 2017.
Lars Birkedal is a Fellow of the ACM, an elected member of the Royal Danish Academy of Sciences and Letters, the recipient of a Villum Investigator grant from the Villum Foundation 2019, the Danish Minister of Research Elite Research Award 2015, and the ACM SIGPLAN Milner Award 2013. Lars Birkedal’s main research interests lie in the area of logic and semantics of programming languages and type theories. Current work focuses on program logics for reasoning about concurrent, higher-order, and imperative programs; cyber-security; and type theories with guarded recursion.
Host: Martin Odersky and Viktor Kuncak
Total Functions: How and Why
26.11.2021, 22:22
Semantics and Verification of Concurrency
26.11.2021, 12:07
Jérôme Boillot: Abstract Interpretation in Stainless
22.11.2021, 17:21
Omega Continuity, Galois Connection, and AI Recipe
18.11.2021, 18:30
13-01-Live1, From Lattice Products to Tarski's Fixedpoint Theorem
18.11.2021, 18:27
12-02-Live2, Lattices for Abstract Interpretation
11.11.2021, 21:37
12-01, Abstract Interpretation Idea
11.11.2021, 21:31
11-01-Live1, Introduction to SMT Solving
04.11.2021, 21:07
10-03, Recursion 2
29.10.2021, 17:05
10-02, Approximating Loops. Recursion 1
29.10.2021, 17:04
10-01, Loop Semantics Example
29.10.2021, 17:01
09-02, Relational Semantics of Loops
28.10.2021, 17:22
09-01, Monotonicity and Semantics of Local Variables
28.10.2021, 17:18
07-03-Live3, Hoare Logic, Strongest Postcondition, Weakest Precondition Part 2
22.10.2021, 21:29
07-02-Live2, Hoare Logic, Strongest Postcondition, Weakest Precondition Part 1
21.10.2021, 22:52
07-01-Live1, Converting Imperative Programs to Formulas
21.10.2021, 22:50
06-02-Live2, Automating First-Order Logic Proofs Using Resolution 2
16.10.2021, 23:21
06-01-Live1, Automating First-Order Logic Proofs Using Resolution 1
16.10.2021, 23:20
05-02-Live2, Quantifier Elimination Steps for Presburger Arithmetic
08.10.2021, 23:12
05-01-Live1part, Introduction to Quantifier Elimination for Presburger Arithmetic
08.10.2021, 23:10
03-02-Live4, Propositional Resolution and SAT Solvers, Live2
07.10.2021, 23:57
03-02-Live3, Case Analysis Rule and Propositional Resolution, Live1
07.10.2021, 23:55
03-02-Live2, Soundness and Completeness of a Propositional Proof System
01.10.2021, 22:54
03-01-Live1, Checking invariants and bounded model checking. What is a formal proof?
01.10.2021, 22:48
02-02-Live2, Finite Systems Expressed with Formulas
30.09.2021, 22:46
02-01-Live, Dispenser Example and its Stainless Representation
30.09.2021, 22:44
01-03-Live3, Disasters, Successes, and Inductive Invariants
24.09.2021, 12:30
01-02-Live2, Introduction to Stainless
24.09.2021, 12:26
01-01-Live1, Introduction to Formal Verification
24.09.2021, 12:14
Live recording of lecture 01 of Formal Verification EPFL course, as given on 2021-09-23 from 15:15-16:45.
08-01, Hoare Logic, Strongest Postcondition, Weakest Precondition
19.11.2020, 00:50
07-01, Converting Imperative Programs to Formulas
28.10.2020, 23:29
06-01, Automating First-Order Logic Proofs Using Resolution
22.10.2020, 16:37
05-02, Quantifier Elimination Steps for Presburger Arithmetic
15.10.2020, 00:20
05-01, Presburger Arithmetic and Quantifier Elimination Introduction
14.10.2020, 21:28
04-01, Simulation Relations
08.10.2020, 17:09
03-20, Short Coq Tutorial
02.10.2020, 14:46
Recording of the Coq tutorial presented on Friday 02/10/20.
03-02, Propositional Resolution
01.10.2020, 03:48
03-01, What is a Formal Proof?
30.09.2020, 19:30
02-02, Finite Systems Expressed with Formulas
24.09.2020, 02:33
02-01, Dispenser Example of Finite System
24.09.2020, 01:29
01-05, Disasters, Successes, and Inductive Invariants
17.09.2020, 04:03
01-04, Unfolding recursive functions in Stainless
17.09.2020, 02:04
01-03, Auxiliary Assertions in Stainless
16.09.2020, 22:12
01-02, First Steps with Stainless
13.09.2020, 00:22
50-01, Specification and Verification of a Blockchain Light Client
11.09.2020, 16:32
00-01, About the instructor (Jad Hamza)
10.09.2020, 11:55
01-21, Stainless Tutorial 1/4
09.09.2020, 11:17
https://github.com/epfl-lara/stainless/releases
Important: you must have Java 8 installed (other versions of Java might make Stainless crash)
01-01, What is Formal Verification?
09.09.2020, 11:15
00-00, About the instructor (Viktor Kuncak)
08.09.2020, 10:42
Viktor Kuncak (http://lara.epfl.ch/~kuncak/) is an associate professor (with tenure) in the School of Computer and Communication sciences of EPFL (Ecole Polytechnique Federale de Lausanne). He joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.