Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Formal methods

Related lectures (29)

Protocols: Formal Description and Session Types

Covers protocols, formal descriptions with session types, message types, and linear logic.

Introduction to Formal Verification

Introduces formal verification, emphasizing rigorous proof of system correctness and the use of mathematical models.

Formal Verification Course Introduction

Introduces the formal verification course by the instructor, who encourages students to enjoy writing proofs.

Automated Reasoning: Formal Verification with LISA

Explores formal verification using the LISA proof assistant and the OCBSL Equivalence Checker.

Memory Model

Explores the formalization of memory models and their crucial role in program optimization.

Compiler verification: Challenges and Benefits

Explores the challenges and benefits of compiler verification, emphasizing the importance of verifying compilers for critical software.

Specification and Verification of a Blockchain Light Client

Covers the design, implementation, and formal verification of distributed systems, focusing on verifiable distributed systems and organizations.

Timing and Performance Analysis: Model Checking

Covers timing and performance analysis using model checking and multiple objective scheduling.

Student Evaluation of Teaching: Importance and Methods

Explores the significance of student feedback on teaching and the methods to collect it.

First Steps with Stainless

Introduces Stainless, a verifier for Scala, emphasizing bug prevention and library access.

Martingale-based Methods for Stochastic Systems

Explores martingales in stochastic systems, focusing on formal analysis, termination analysis, and stability verification.

Introduction to Quantifier Elimination for Presburger Arithmetic

Introduces formal verification methodology and Presburger arithmetic for program verification and automated reasoning.

Stochastic Hybrid Systems

Explores time-determinator model checking, U-Pool scheduling, worst-case execution time analysis, and statistical model checking for cyber-physical systems.

Correctness of Compilers: Part 1

Explores compiler correctness, examples of verified compilers, formal verification, and the challenges of certifying compilers.

Verified Functional Programming: Nicolas Voirol public PhD thesis defense

Explores verified functional programming, formal verification, SMT solvers, type checking, Scala features, automation, and dependent types.

What is Formal Verification?

Introduces formal verification and its advantages over traditional testing methods, discussing automated theorem proving and compiling correctness statements into verification conditions.

Formal Analysis: Classic Waffle Iron 3x3

Explores the formal analysis of a classic waffle iron design evolution.

Stainless Verification System Tutorial

Introduces Stainless, an open-source tool for verifying Scala programs, covering language, modeling, verification tips, and inner workings.

Formally Correct Intermittent Systems Log in to Mediaspace to watch this video

Focuses on designing formally correct intermittent systems in batteryless systems powered intermittently, addressing challenges and strategies for ensuring correctness.

Software Correctness: Testing and Verification Log in to Mediaspace to watch this video

Explores software correctness through testing, verification, property-based fuzzing, and dynamic information flow control.