ACM SIGPLAN Courses

Verification-Preserving Inlining in Automatic Separation Logic Verifiers

Explore verification-preserving inlining techniques for automatic separation logic verifiers, enhancing bounded verification without requiring extensive annotations.

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

Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction

Explore Vulcan, a framework enhancing language-agnostic program reducers through diverse transformations, outperforming state-of-the-art tools in minimizing bug-triggering programs across multiple languages.

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

Data Extraction via Semantic Regular Expression Synthesis

Explore semantic regexes for advanced data extraction, combining syntactic and semantic reasoning. Learn about a novel algorithm synthesizing these regexes from minimal examples.

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

Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates

Explore an innovative approach to synthesizing relational queries with recursion and invented predicates, outperforming state-of-the-art baselines in runtime and accuracy.

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

Leaf: Modularity for Temporary Sharing in Separation Logic

Explore a novel approach to handling temporarily shared state in concurrent verification using Leaf, a library in Iris separation logic. Learn about guarding operators and their application in verifying reader-writer locks and hash tables.

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

Saggitarius: A DSL for Specifying Grammatical Domains

Explore Saggitarius, a new DSL for specifying grammatical domains. Learn how it helps programmers reason about data formats and infer grammars for various representations of common data types.

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

From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers

Explore efficient compilation of lexical effect handlers through a novel method of inferring lifting information, bridging capabilities and regions for improved runtime performance.

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

Message Chains for Distributed System Verification

Explore an automated bookkeeping method using message chains to simplify verification of asynchronous distributed programs, revealing execution structure and aiding in system-level reasoning.

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

Greedy Implicit Bounded Quantification in Object-Oriented Programming Languages

Explore greedy implicit bounded quantification in object-oriented programming, focusing on type inference algorithms and a variant of kernel F≤ with implicit polymorphism.

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

Validating IoT Devices with Rate-Based Session Types

Explore a novel framework for implementing and validating rate-based message passing systems in IoT domains using session types, ensuring rate error freedom and type preservation.

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

Synthesizing Efficient Memoization Algorithms

Explore an automated approach for synthesizing efficient memoization algorithms from declarative specifications, addressing challenges through novel synthesis techniques and evaluation on real-world benchmarks.

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

Equality Saturation Theory Exploration à la Carte

Explore Enumo, a new language for programmable theory exploration in equality saturation. Learn to guide rule inference, build rulesets, and develop strategies for optimizing compilers and synthesizers.

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

Resource-Aware Soundness for Big-Step Semantics

Explore resource-aware extensions to lambda calculus semantics and type systems, ensuring well-typed programs avoid resource exhaustion through coinductive reasoning and big-step formalization.

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

Accelerometers as an Instrument in Electronic Music Performance

Explore integrating motion sensing and accelerometers in electronic music performances, focusing on expressiveness and technical solutions.

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

Runtime Detection of Data Races in OCaml with ThreadSanitizer

Explore runtime detection of data races in OCaml using ThreadSanitizer. Learn core principles, challenges, adaptations, and practical application for reliable parallel code development.

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