ACM SIGPLAN Courses

Flux: Liquid Types for Rust

Explore Flux, a refined type system for Rust that enhances verification of low-level pointer programs. Learn how it combines logical refinements with Rust's ownership mechanisms for efficient and ergonomic type-based verification.

• YouTube
• 20 minutes
• On-Demand
• Free Video

Recursive State Machine Guided Graph Folding for Context-Free Language Reachability

Explore an innovative approach to improve CFL-reachability scalability through graph folding, reducing input size and enhancing performance in program analysis applications like alias and value-flow analysis.

• YouTube
• 15 minutes
• On-Demand
• Free Video

Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning

Explore Zar: a verified compiler for discrete probabilistic programs, transforming cpGCL to executable samplers. Learn about choice-fix trees, interaction trees, and sampling equidistribution theorem.

• YouTube
• 20 minutes
• On-Demand
• Free Video

Garbage-Collection Safety for Region-Based Type-Polymorphic Programs

Explore a novel region type-system for ensuring garbage-collection safety in polymorphic programs, addressing soundness issues and enabling efficient memory management strategies.

• YouTube
• 18 minutes
• On-Demand
• Free Video

Feature-Sensitive Coverage for Conformance Testing of Programming Language Implementations

Explore novel coverage criteria for generating high-quality conformance tests in programming language implementations, focusing on feature-sensitive and feature-call-path-sensitive approaches.

• YouTube
• 19 minutes
• On-Demand
• Free Video

Psym: Efficient Symbolic Exploration of Distributed Systems

Explore efficient symbolic methods for verifying distributed systems using Psym, a tool that avoids redundant states, interleavings, and computations during exploration.

• YouTube
• 18 minutes
• On-Demand
• Free Video

One Pixel Adversarial Attacks via Sketched Programs

Explore a novel approach for one-pixel adversarial attacks using program synthesis, achieving state-of-the-art success rates with fewer queries and transferable programs for neural network classifiers.

• YouTube
• 19 minutes
• On-Demand
• Free Video

Repairing Regular Expressions for Extraction

Explore a novel method for synthesizing and repairing regular expressions for extraction, addressing challenges with real-world extensions and deterministic behavior of regex engines.

• YouTube
• 17 minutes
• On-Demand
• Free Video

Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs

Discover a novel technique for detecting vulnerabilities in zero-knowledge proof circuits, combining SMT solving with uniqueness inference to enhance security in blockchain applications.

• YouTube
• 19 minutes
• On-Demand
• Free Video

Merging Inductive Relations for Improved Program Specification

Explore an algorithm for merging inductive relations, improving automatic generation performance and simplifying mechanized proofs in proof engineering tools like QuickChick for Coq.

• YouTube
• 19 minutes
• On-Demand
• Free Video

Trace-Guided Inductive Synthesis of Recursive Functional Programs

Explore a novel trace-guided approach for synthesizing recursive functional programs from input-output examples, addressing ambiguity and generalization challenges in program synthesis.

• YouTube
• 20 minutes
• On-Demand
• Free Video

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

Explore robust and modular verification of WebAssembly programs using Iris-Wasm, a mechanized higher-order separation logic for specifying and verifying individual modules with strong isolation guarantees.

• YouTube
• 16 minutes
• On-Demand
• Free Video

Synthesizing MILP Constraints for Efficient and Robust Optimization

Explore a novel syntax-guided synthesis method for generating high-quality MILP constraints from Boolean logic specifications, improving efficiency and robustness in optimization problems.

• YouTube
• 17 minutes
• On-Demand
• Free Video

Lilac: A Modal Separation Logic for Conditional Probability

Explore Lilac, a novel separation logic for probabilistic programs, introducing a modality for conditional probability reasoning and validating its effectiveness through formal verification examples.

• YouTube
• 19 minutes
• On-Demand
• Free Video

CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives

Explore CryptOpt, a verified compilation pipeline for cryptographic primitives that generates high-performance assembly code with formal proofs, outperforming GCC and Clang for specific applications.

• YouTube
• 19 minutes
• On-Demand
• Free Video