Concept
Formal verification
Related lectures (82)
Stainless Tutorial: Verification of Scala Code
Covers the use of Stainless, a verification tool for Scala, to ensure the correctness of Scala code.
Invariants in Bounded Counter: Understanding Inductive Invariants
Explores invariants in a bounded counter system and the significance of inductive invariants in verifying system properties.
Verifying Programs with Stainless: An Extended Example
Explores program verification using Stainless with a focus on the Quite OK Image Format (QOI) and its Scala implementation.
First Steps with Stainless
Introduces Stainless, a verifier for Scala, emphasizing bug prevention and library access.
Introduction to Quantifier Elimination for Presburger Arithmetic
Introduces formal verification methodology and Presburger arithmetic for program verification and automated reasoning.
Memory Model
Explores the formalization of memory models and their crucial role in program optimization.
Simulation Relations
Covers transition systems, behavior equivalence, and system refinement for system modeling and verification.
Formal Verification and Program Synthesis
Explores Viktor Kuncak's research in formal verification, program synthesis, and teaching activities at EPFL.
5G Authentication: Security and SUKI
Explores the evolution of 5G authentication, vulnerabilities in 4G, and improvements in 5G security.
Presburger Arithmetic and Quantifier Elimination
Covers Presburger arithmetic, quantifier elimination, and the transformation of formulas into disjunctive normal form.