ACM SIGPLAN Courses

Complete First-Order Reasoning for Properties of Functional Programs - OOPSLA 2023

Explore complete first-order reasoning for functional program properties, uncovering theoretical foundations of verification tools and explaining their efficacy, limitations, and user assistance role.

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

Accelerating Fuzzing through Prefix-Guided Execution

Explore prefix-guided execution for accelerating coverage-guided fuzzing, improving bug detection and code coverage in software testing through early termination of unlikely tests.

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

Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving

Explore innovative concrete type inference for dynamically typed languages, combining machine learning and SMT solving to enable code optimization without manual type annotations, significantly boosting performance.

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

Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data

Explore Secure RDTs for enforcing role-based access control on offline-available JSON data, enhancing security in applications with intermittent network connectivity.

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

Synthesizing Specifications - Automatic Generation of Program Behavior Descriptions

Explore automatic synthesis of program specifications using Spyro, a tool that generates precise L-properties based on user queries and domain-specific languages, applicable in various programming contexts.

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

Reference Capabilities for Flexible Memory Management

Explore Verona's innovative approach to memory management using isolated regions and reference capabilities, enabling predictable and controlled memory use in concurrent programming.

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

Mutually Iso-Recursive Subtyping - OOPSLA 2023

Explore mutually iso-recursive subtyping, addressing challenges in type recursion for programming languages. Gain insights into efficient type checking and subtyping for intermediate code representations.

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

Type-Safe Dynamic Placement with First-Class Placed Values

Explore type-safe dynamic placement in distributed systems using first-class placed values. Learn about Dyno, a language enabling static reasoning with dynamic placement flexibility.

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

Optimization-Aware Compiler-Level Event Profiling

Explore a novel technique for quantifying compiler-internal events in optimized code, reducing profiling perturbation and enhancing dynamic analysis accuracy.

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

Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols

Explore a novel interactive verification methodology using relational abstraction to tackle quantifier reasoning challenges in infinite-state systems, with applications to distributed protocols.

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

MemPerf: Profiling Allocator-Induced Performance Slowdowns

Explore MemPerf, a novel profiler for identifying allocator-induced performance slowdowns. Learn about life-cycle based detection, thread-aware modeling, and unified methods for pinpointing memory access issues.

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

Verus: Verifying Rust Programs Using Linear Ghost Types

Explore Verus, an SMT-based tool for formally verifying Rust programs. Learn how it leverages Rust's linear types and borrow checking to prove functional correctness in low-level, high-assurance systems.

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

Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems

Explore efficient Boolean unification for Hindley-Milner-style type and effect systems. Learn about a hybrid algorithm improving compilation speed and reducing inference overhead in polymorphic effect systems.

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

Synthesizing Precise Static Analyzers for Automatic Differentiation

Explore Pasado, a technique for synthesizing precise static analyzers for Automatic Differentiation, improving precision in nonlinear operations and demonstrating applications in various domains.

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

Automated Translation of Functional Big Data Queries to SQL

Explore automated translation of functional big data queries to SQL, improving efficiency while maintaining abstraction benefits. Learn about novel column-wise decomposition for query synthesis.

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