ACM SIGPLAN Courses

Allo: A Programming Model for Composable Accelerator Design

Explore Allo, a composable programming model for efficient spatial accelerator design. Learn how it decouples hardware customizations and preserves hierarchical structure for holistic optimizations across function boundaries.

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

SpEQ: Translation of Sparse Codes using Equivalences

Explore SpEQ, a strategy for translating sparse linear algebra codes to high-performance libraries. Learn about detecting semantics, identifying computations, and ensuring correct translations with runtime checks.

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

Consolidating Smart Contracts with Behavioral Contracts

Explore ConSol, a Solidity extension enhancing smart contract reliability through behavioral contracts. Learn to express critical conditions, prevent attacks, and improve code robustness and readability.

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

SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques

Explore novel superoptimization techniques for stack-bytecode, combining greedy algorithms, MaxSAT representation, and domain-specific constraints to enhance optimization gains and reduce processing time.

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

Compiling with Abstract Interpretation

Explorez l'intégration de l'interprétation abstraite dans la compilation, améliorant la précision des analyses statiques et permettant des transformations de programme efficaces.

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

SMT Theory Arbitrage: Approximating Unbounded Constraints Using Bounded Theories

Explore SMT theory arbitrage for transforming unbounded constraints into bounded ones, improving solver performance and enabling optimization techniques for bounded theories.

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

Reducing Static Analysis Unsoundness with Approximate Interpretation

Explore a novel dynamic analysis technique for JavaScript that improves static analysis accuracy, particularly for dynamic property accesses, enhancing call graph construction and analysis recall.

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

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language

Explore a novel validation methodology for automated program verifiers, ensuring soundness through formal semantics and proof generation in Isabelle, with focus on Viper and Boogie languages.

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

Floating-Point TVPI Abstract Domain for Numerical Program Analysis

Explore an efficient numerical abstract domain for analyzing floating-point programs, supporting conditionals, loops, and elementary functions. Learn about TVPI-FP's innovative use of interval arithmetic in inequalities.

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

Automated Verification of Fundamental Algebraic Laws - PLDI 2024

Explore automated verification of algebraic laws in coding, crucial for software correctness. Learn about Propel verifier's capabilities in proving properties across various domains.

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

A Verified Compiler for a Functional Tensor Language - PLDI 2024

Explore a verified compiler for functional tensor language, focusing on efficient array code production and formal correctness proof for high-performance domains like image processing and machine learning.

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

Qubit Recycling Revisited - Optimizing Quantum Circuit Width

Explore qubit recycling optimization for quantum circuits, focusing on complexity, algorithms, and verification using qubit dependency graphs and matrix triangularization techniques.

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

De/Re-Composition of Data-Parallel Computations via Multi-Dimensional Homomorphism - PLDI 2024

Explore a systematic approach for efficient (de/re)-composition of data-parallel computations using Multi-Dimensional Homomorphisms, applicable to various architectures and outperforming state-of-the-art solutions.

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

Syntactic Code Search with Sequence-to-Tree Matching: Supporting Syntactic Search with Incomplete Code Fragments

Explore a novel syntactic code search approach using sequence-to-tree matching, enabling tree-aware wildcards and supporting incomplete code fragments for more flexible and interactive searching.

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

Quantitative Robustness for Vulnerability Assessment

Explore quantitative robust reachability for measuring bug triggering difficulty in software security. Learn about QRSE and functional E-MAJSAT for improved vulnerability assessment.

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