ACM SIGPLAN Courses

A Hoare Logic for Symmetry Properties

1 rating

Discover a novel Hoare-style logic for verifying symmetry properties in imperative programs using group actions, with practical tool SymVerif for formal verification.

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

Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training

1 rating

Explore a novel approach for quantitatively verifying probabilistic Deep Reinforcement Learning policies through abstract training, addressing challenges in neural network reasoning and state explosion in safety-critical applications.

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

Machine Checked Proofs and Programs in Algebraic Combinatorics

Explore a Coq/Rocq library formalizing symmetric functions and character theory, featuring the Littlewood-Richardson rule proof and highlighting the interplay between algorithms and algebraic constructions in combinatorics.

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

CRIS: The Power of Imagination in Specification and Verification

Explore CRIS, a novel verification tool that introduces imaginary specifications to program verification, unifying separation logic and program refinement approaches for simplified proof decomposition.

• YouTube
• 1 hour 3 minutes
• Self-Paced
• Free Video

CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq

Discover a verified WebAssembly backend for CertiCoq that produces efficient programs, implements Coq's primitive integer operations, and demonstrates practical applications for web programs and blockchain smart contracts.

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

Tactic Script Optimisation for Aesop

Discover how to transform naive tactic scripts into human-like proofs with a three-stage optimization pipeline for Aesop in Lean, improving readability and efficiency in interactive theorem proving.

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

A CHERI C Memory Model for Verified Temporal Safety

Explore a formal approach to temporal memory safety in CHERI C, examining capability revocation mechanisms, introducing pointer provenance tracking, and defining security guarantees with Coq-verified memory state invariants.

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

Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR

Explore monadic interpreters using Choice Tree (CTree) library to formalize semantics for concurrency and weak memory models in LLVM IR, with executable results and proven equivalences between memory models.

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

An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting

Explore the Isabelle/HOL formalization of co-rewrite pairs for non-reachability analysis in term rewriting, including polynomial interpretations over negative integers and weighted path order implementations.

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

Formalized Burrows-Wheeler Transform

Discover the first formal verification of the Burrows-Wheeler Transform and its inverse in Isabelle/HOL, ensuring correctness for this critical algorithm used in compression software and genomic data analysis.

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

Verified and Efficient Matching of Regular Expressions with Lookaround

Explore a Coq formalization of regular expressions with lookarounds, featuring a verified linear-time matching algorithm and experimental results supporting its efficiency and correctness.

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

Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems

Explore the formalization of a sufficient condition for confluence in first-order left-linear rewrite systems using simultaneous critical pairs, extending beyond development-closed critical pairs.

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

Prospects for Computer Formalization of Infinite-Dimensional Category Theory

Explore the challenges and collaborative efforts in formalizing infinite-dimensional weak category theory using Lean and Rzk proof assistants, with insights on contributing to this mathematical advancement.

• YouTube
• 1 hour
• Self-Paced
• Free Video

Nominal Matching Logic With Fixpoints

Explore nominal matching logic with fixpoints and learn how alpha-structural induction principles can be derived to prove properties of languages with binders, demonstrated through λ-calculus examples using Metamath Zero.

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

An Isabelle/HOL Framework for Synthetic Completeness Proofs

Explore an abstract framework in Isabelle/HOL for mechanizing completeness proofs across different logics, featuring a transfinite version of Lindenbaum's lemma and techniques for building maximal consistent sets.

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