ACM SIGPLAN Courses

Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra

Explore a three-dimensional refinement algebra framework that unifies compositional verification and certified compilation for large-scale, heterogeneous systems, demonstrated through multiple use cases in Coq.

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

On Extending Incorrectness Logic with Backwards Reasoning

Explore an extension of incorrectness logic that enables backwards reasoning through underspecification, combining underapproximation with formal proofs and loop summaries, all verified in Isabelle/HOL.

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

Enhancing Network Diagnosis with Reflection in Prolog - Extended Abstract

Explore how reflection in Prolog can improve network diagnosis by enabling reasoning about both network states and the reasoning process itself, particularly for complex real-world networks.

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

The Best of Abstract Interpretations

Explore the theoretical foundations of "the best of abstract interpretations" in program analysis, examining computability properties and proving techniques for optimal abstract interpretations.

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

Linear and Non-linear Relational Analyses for Quantum Program Optimization

Discover how phase folding optimization can be reframed as affine relation analysis, extending quantum circuit optimization to programs with complex control flow and enabling non-linear relation analysis for improved compiler performance.

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

ASP for Language Documentation and Reclamation: A Derivational Stemming Tool for Myaamia

Explore how Answer Set Programming (ASP) is applied to develop a derivational stemming tool for the Myaamia language, supporting documentation and reclamation efforts for this reawakening Algonquian language.

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

Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs

Explore algebraic temporal effects for verifying temporal safety and liveness properties in higher-order programs with recursive types, featuring novel approaches using later modality and demonstrations with concurrent programs.

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

MOLA: A Runtime Verification Engine Factory by Meta-interpreting Embedded DSLs

Discover MOLA, a universal interpreter for Stream Runtime Verification that offers data-theory extensibility, type guarantees, and simplified syntax with improved error reporting, separating datatypes from temporal engines.

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

BeePL: Correct-by-Compilation Kernel Extensions

Discover BeePL, a new eBPF programming language with a type system that encodes specifications and a formally verified compiler, enabling safer kernel extensions without modifying kernel source code.

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

Leveraging Duality for Programming with zkSNARKs

Explore how to simplify zkSNARK programming through a new language feature that leverages the duality between proof construction and verification, enabling code reuse and easier maintenance.

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

Interaction Equivalence

Explore interaction equivalence in lambda calculus, a novel approach to program equivalence that counts interaction steps between terms and contexts while preserving equational theory properties.

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

Enhancing a Hierarchical Graph Rewriting Language Based on MELL Cut Elimination

Explore how hierarchical graph rewriting language LMNtal can be extended using MELL proof nets, enabling operations on Promotion Boxes and creating a practical platform for modeling and verification.

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

Automated Playing of Survival Video Games with Commonsense Reasoning

Explore how answer set programming and commonsense reasoning can automate gameplay in the survival game Don't Starve, creating an agent that outperforms novice players through environmental learning and logical decision-making.

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

Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning

Discover Bluebell, a program logic unifying unary and relational reasoning styles for probabilistic programs through "joint conditioning" - connecting conditional independence with relational liftings for enhanced verification capabilities.

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

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