ACM SIGPLAN Courses

PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams

Explore PfComp, a verified compiler for stateless firewall policies using binary decision diagrams. Learn about its Coq-assisted proof, OCaml extraction, and performance benefits.

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

Displayed Monoidal Categories for the Semantics of Linear Logic

Explore formalized categorical structures for linear logic interpretation using UniMath. Learn about displayed monoidal categories and their application in constructing complex instances.

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

Memory Simulations, Security and Optimization in a Verified Compiler

Explore memory simulations, security features, and optimizations in verified compilers. Gain insights into pointer allocations, stack canaries, and tail recursion elimination in CompCert.

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

Under-approximation for Scalable Bug Detection

Explore under-approximation techniques for efficient bug detection in large codebases. Learn about Incorrectness Logic, ISL, and Pulse-X for scalable, compositional program analysis and memory safety error detection.

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

Martin-Löf Type Theory Mechanization in Coq

Explore an extensive mechanization of Martin-Löf Type Theory in Coq, covering decidability of conversion and type checking, with a certified executable type checker for MLTT.

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

Improved Assistance for Interactive Proof - Machine Learning in Theorem Proving

Explore machine learning techniques enhancing interactive theorem provers, from established methods to emerging challenges in automation and efficient interaction.

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

The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography

Explore foundational end-to-end verification of high-speed cryptography, connecting Hacspec, Jasmin, and SSProve tools using Coq. Demonstrates approach with AES implementation proof.

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

Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma

Explore formal probabilistic methods for combinatorial structures, focusing on the Lovász Local Lemma and its application to hypergraph coloring in Isabelle/HOL.

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

Working with Peter O'Hearn in Academia and Industry

Explore Mark Harman's experiences collaborating with Peter O'Hearn across academic and industrial settings, gaining insights into their influential work.

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

Peter, the May and the Must, and Lacework

Explore Peter O'Hearn's contributions to program analysis and verification, focusing on the "may" and "must" concepts and Lacework's impact.

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

Massive Proofs for the Masses

Explore massive proofs and their applications in computer science with Byron Cook's insightful presentation on cutting-edge verification techniques.

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

Bi-abductive Adversarial Program Synthesis

Explore bi-abductive adversarial program synthesis techniques in this advanced computer science talk by Julien Vanegue.

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

Symbolic Execution with Separating Decision Diagrams

Explore symbolic execution techniques using Separating Decision Diagrams in this advanced computer science talk by Josh Berdine.

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

Is Peter Correct or Incorrect? - O'HearnFest Lecture

Explore Patrick Cousot's analysis of Peter O'Hearn's work in program verification and reasoning, examining correctness and potential inaccuracies in his theories.

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

Can We Reason About the Security of Concurrent Systems Code?

Explore challenges and possibilities in reasoning about security in concurrent systems code with expert Peter Sewell.

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