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

Concept

Formal verification

Related lectures (29)

Memory Model

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

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.

Dependable Architectures and Software Log in to Mediaspace to watch this video

Explores dependable architectures, error detection, fault-tolerant structures, and software reliability through examples like the Patriot Missile failure and ABB dual controller.

Property-Based Testing: QuickChick Log in to Mediaspace to watch this video

Explores property-based testing using QuickChick, focusing on software correctness, specifications, and dynamic information flow control.

Designing Provably Performant Networked Systems Log in to Mediaspace to watch this video

Explores the design of networked systems for robust performance, emphasizing real-time applications and formal verification.

Hardware Verification using High-Level Design Languages Log in to Mediaspace to watch this video

Explores challenges in hardware verification, clear specifications, speculation harm, and cycle-precise semantics.

Purely Functional Priority Queue Log in to Mediaspace to watch this video

Covers optimal purely functional priority queues, Scala implementation, Stainless integration, operations properties, and binomial queues.

Encoder and Decoder for Prefix-Free Codes Log in to Mediaspace to watch this video

Covers the implementation and verification of encoder and decoder for prefix-free codes, including classes and types, lemmas on trees, and the main theorem.

SecChisel: Security Verification of Secure Processor Architectures Log in to Mediaspace to watch this video

Presents the SecChisel framework for verifying security properties of secure processor architectures at design-time.