ACM SIGPLAN Courses

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

Dafny as Verification-Aware Intermediate Language for Code Generation

Explore how formal methods can improve LLM code generation by using Dafny as an intermediate language to validate correctness before compiling to target languages.

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

Baking for Dafny: A CakeML Backend for Dafny

Explore the development of a CakeML backend for Dafny that aims to reduce the trusted computing base by translating Dafny programs to CakeML, a verified subset of Standard ML, with functional big-step semantics.

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

Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean

Explore a methodology for handling complex Dafny program verification using Lean's interactive theorem prover, extracting straight-line programs and embedding Dafny's semantics to overcome automation limitations.

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

DafnyBench: A Benchmark for Formal Software Verification

Discover DafnyBench, the largest benchmark for training and evaluating ML systems in formal software verification, testing LLMs' ability to generate annotations for Dafny verification across 750+ programs.

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