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)

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.

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.

Finite State Machines (FSMs)Log in to Mediaspace to watch this video

Explores Finite State Machines (FSMs) in digital system design, covering Mealy and Moore FSMs, state diagrams, VHDL implementation, and state encoding.

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

Explores designing formally correct intermittent systems for extreme edge computing platforms, emphasizing correctness, reliability, and security.

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.

Concurrency and transactional memory in Dafny Log in to Mediaspace to watch this video

Covers Dafny basics, modeling concurrency, and implementing transactional memory with safety and liveness proofs.

Separation is all you need: Foundations for Modular Verification Log in to Mediaspace to watch this video

Explores the foundations of modular verification using Separation Logic for realistic concurrent programs and discusses the challenges of shared mutable state in concurrency.