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

Lecture

Formal Verification and Program Synthesis

Related lectures (30)

Explores Viktor Kuncak's research in formal verification, program synthesis, and teaching activities at EPFL.

Covers the basics of concurrency, its importance, and how to write concurrent programs.

Presents an algorithm to prevent starvation and maximize philosophers eating simultaneously.

Covers Akka Streams basics, stream stages concurrency, materialized values, and more.

Covers the basics of atomic operations in concurrency and parallelism, including hardware-provided operations and synchronized algorithms.

Explores visibility in concurrency, memory models, shared memory, and hardware optimizations.

Discusses algorithms to prevent starvation and maximize philosophers eating simultaneously.

Explains the Sequential Consistency model in concurrency and parallelism, covering program order, atomicity, and performance implications.

Explores thread safety, synchronization, and concurrent collections in Scala, focusing on a lock-free concurrent queue implementation.

Introduces Coq and focuses on proving the theorem and_comm step by step.

Covers the course CS206 on Parallelism and Concurrency, including logistics, materials, exercise sessions, labs, exams, and grading criteria.

Explores concurrency semantics, recursive functions, loops, interleaving modeling, and interpreter verification.

Explains the Java Memory Model and thread start semantics for concurrent programs.

Introduces the readers-writer lock for handling concurrency in scenarios with frequent reads and occasional updates.

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

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

Covers the basics of concurrency, focusing on threads and synchronization, including thread joining and challenges of non-deterministic execution.

Explores automatic optimization of arithmetic circuits, addressing challenges in restructuring circuits for improved efficiency and performance.

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