ACM SIGPLAN Courses

Symbolic Automata: Omega-Regularity Modulo Theories

Explore the generalization of symbolic automata to support ω-regular languages through symbolic transition terms and derivatives, unifying classic automata and logics for symbolic model checking applications.

• YouTube
• 20 minutes
• Self-Paced
• Free Video

Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting

Discover Archmage, a framework enabling end-to-end verification for programs with integer-pointer casts, alongside CompCertCast and Archmage logic for practical implementation and reasoning in verified compilation chains.

• YouTube
• 21 minutes
• Self-Paced
• Free Video

Solvers, Unite! A Simple Unified Semantics for Reasoning with Assurance and Agreement

Explore a unified semantics for complex reasoning problems with logic rules, recursion, and aggregation, showing how different solver classes can be combined for enhanced problem-solving capabilities.

• YouTube
• 58 minutes
• Self-Paced
• Free Video

Formal Foundations for Translational Separation Logic Verifiers

Explore a formal framework for reasoning about translational separation logic verifiers, featuring a generic core IVL that connects input programs with back-end verifiers through operational semantics and angelic non-determinism.

• YouTube
• 21 minutes
• Self-Paced
• Free Video

Formalising Graph Algorithms with Coinduction

Explore a formal theory of graphs as coinductive structures in Agda, addressing challenges in formalizing graph algorithms with dependently-typed proof assistants through innovative quotient types and reusable techniques.

• YouTube
• 21 minutes
• Self-Paced
• Free Video

BiSikkel: A Multimode Logical Framework in Agda

Explore BiSikkel, a multimode logical framework in Agda that extends the Sikkel library with capabilities for writing multimode proofs about multimode programs, demonstrated through guarded streams and parametricity predicates.

• YouTube
• 20 minutes
• Self-Paced
• Free Video

SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations

Explore a novel proof method for preserving non-interference across compiler transformations under speculative semantics, revealing security weaknesses in register allocation and proposing automated fixes.

• YouTube
• 22 minutes
• Self-Paced
• Free Video

On Bridging Prolog and Python to Enhance an Inductive Logic Programming System

Explore how researchers developed a Prolog-Python interface that combines Prolog's deduction capabilities with Python's extensive libraries, enhancing an Inductive Logic Programming System with visualization features.

• YouTube
• 28 minutes
• Self-Paced
• Free Video

Towards Mining Robust Coq Proof Patterns

Discover how mining robust Coq proof patterns can adapt software engineering repair approaches to reduce human effort in maintaining formal proof scripts, with insights from the University of Melbourne team.

• YouTube
• 19 minutes
• Self-Paced
• Free Video

Performant, Readable and Interoperable Rust from Dafny

Discover a novel Dafny-to-Rust compiler that generates efficient, readable Rust code while bridging formal verification with high performance, featuring competitive benchmarks and solutions for type system and memory management challenges.

• YouTube
• 17 minutes
• Self-Paced
• Free Video

Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny

Explore the formal verification of regular expressions in Dafny, demonstrating how denotational (inductive) and operational (coinductive) semantics are equivalent through pointwise bisimilarity.

• YouTube
• 19 minutes
• Self-Paced
• Free Video

Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems

Explore Shipwright, a modular framework for verifying liveness in Byzantine fault tolerant systems through refinement techniques, addressing cryptographic signatures, fairness properties, and implementation decomposition.

• YouTube
• 18 minutes
• Self-Paced
• Free Video

Towards Proof Stability in SMT-based Program Verification

Explore the challenges of proof instability in SMT-based verification, where minor source code changes cause verification failures, and learn about methodologies to detect, measure, and mitigate this problem.

• YouTube
• 15 minutes
• Self-Paced
• Free Video

Laurel: Unblocking Automated Verification with Large Language Models

Discover how Laurel uses large language models to automatically generate assertions for program verification, reducing the burden on proof engineers with domain-specific prompting techniques.

• YouTube
• 18 minutes
• Self-Paced
• Free Video

Verifying the Fisher-Yates Shuffle Algorithm in Dafny

Dive into the verification of the Fisher-Yates shuffle algorithm using Dafny, exploring a three-step approach that proves its correctness and ensures unbiased permutation generation.

• YouTube
• 18 minutes
• Self-Paced
• Free Video