ACM SIGPLAN Courses

Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation

Explore modular specification and verification of NOVA microhypervisor using concurrent separation logic. Discover challenges in formally verifying concurrent systems for enhanced virtualization and isolation.

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

Modularizing CPU Semantics for Virtualization

Explore modularization of CPU semantics for efficient virtualization, focusing on simplifying VMM implementation and verification while addressing challenges in hardware-assisted virtualization.

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

All the Binaries Together: A Semantic Approach to Application Binary Interfaces

Explore a semantic approach to Application Binary Interfaces, enhancing interoperability and safety in multi-language systems through realizability models and formalized ABIs.

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

Computational-Bounded Robust Compilation and Universally Composable Security

Explore computational-bounded robust compilation and its connection to universally composable security. Extend techniques to computational UC security and generalize beyond to arbitrary equalities.

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

Secure Calling Conventions for CHERI Capability Machines in Practice - Work in Progress

Explore secure calling conventions for CHERI capability machines, focusing on temporal memory safety and stack frame encapsulation. Evaluate performance impact and compatibility.

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

Teaching Logic and Set Theory with Dafny

Explore logic and set theory concepts using Dafny in a computer science course, enhancing understanding through practical application and verification.

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

CLOVER: Closed-Loop Verifiable Code Generation - Dafny'24

Explore CLOVER, a paradigm for ensuring correctness in AI-generated code through consistency checking among code, docstrings, and formal annotations using verification tools and language models.

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

Verifying a Concurrent File System with Sequential Reasoning

Explore a verified, concurrent file system using GoTxn and Dafny. Learn about crash safety, concurrency, and combining interactive and automated proofs for robust systems software.

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

Debugging Trait Errors as Logic Programs

Explore a proposed trait debugger for Rust, extracting and visualizing proof trees to facilitate debugging of complex trait errors in any domain and scale.

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

Latte: Lightweight Aliasing Tracking for Java

Explore Latte, a lightweight system for tracking aliasing and uniqueness in Java, minimizing annotations and complexity while supporting destructive reads and practical applications.

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

Totally Live Programming with Hazel - Progress Report

Explore Hazel, a groundbreaking live programming environment with error localization and recovery mechanisms, ensuring well-structured and meaningful code at every stage.

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

Diagrammatic Notations for Interactive Theorem Proving

Explore innovative approaches to enrich interactive theorem provers with visual aids, focusing on composable diagram templates for enhanced proof development and presentation.

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

Exploratory Study on Multi-User Program Synthesis - A Multi-Wizard Approach

Explore multi-user program synthesis through a design experiment, investigating collaborative potential and effectiveness in software engineering and related domains.

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

Applying Large Scale Diffing to Declarative Configuration Code for Production Safety

Explore large-scale diffing for declarative configuration code to enhance production safety, addressing unintended consequences and testing challenges in config changes.

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

Ansible Is Turing Complete

Explore Ansible's unexpected Turing completeness through core language features. Discover how this configuration management tool achieves computational universality without relying on external languages or plugins.

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