ACM SIGPLAN Courses

A Hoare Logic for Symmetry Properties

1 rating

Discover a novel Hoare-style logic for verifying symmetry properties in imperative programs using group actions, with practical tool SymVerif for formal verification.

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

Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training

1 rating

Explore a novel approach for quantitatively verifying probabilistic Deep Reinforcement Learning policies through abstract training, addressing challenges in neural network reasoning and state explosion in safety-critical applications.

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

Evolving Weak Memory Models for Evolving Architectures

Explore evolving weak memory models for modern architectures, focusing on advancements and challenges in concurrent programming and hardware design.

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

What Compilers Desire from Weak Memory Semantics

Explore compiler optimization challenges in concurrent programs, focusing on memory models and safety. Investigate deriving models that retain optimization safety across different consistency levels.

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

System-Level Weak Memory Models: The Need for Formalisation, ISA Semantics Integration and Model Diversity

Explore system-level weak memory models, focusing on formalization, ISA semantics integration, and model diversity in computer architecture.

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

Programmers Love Mind-Bogglingly Complicated Weak Memory Models

Explore mind-boggling complexities of weak memory models in programming, delving into their intricacies and implications for software development.

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

Later Credits: A Case Study in the Unreasonable Effectiveness of Separation Logic

Explore the effectiveness of separation logic in software verification through a case study on "Later Credits" presented by Derek Dreyer.

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

Designing Wait-free Weak Reference Counting

Explore wait-free weak reference counting design techniques for efficient memory management in concurrent systems.

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

Lifting Compiler Security Properties to Stronger Attackers: The Speculation Case

Explore compiler security properties against speculative execution attacks, focusing on lifting guarantees to stronger attacker models and developing a formal framework for well-formedness conditions.

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

Domesticating Automation for Large-Scale Verification Systems - Dafny'24

Explore automated theorem proving's potential for scaling verification-based development, focusing on user experience and efficient automation budget management in large-scale systems.

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

Verifying Dafny Contract Integrity - Detecting Common Pitfalls

Detect and prevent common pitfalls in Dafny contracts, including contradictions, vacuity, unconstrained outputs, and redundancy. Enhance software specification accuracy.

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

Testing Specifications in Dafny - Dafny'24

Explore techniques for testing specifications in Dafny, including automatic mutation testing and Spec-Testing Proofs, to enhance trust in formal verification processes.

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

Incremental Proof Development in Dafny with Module-Based Induction

Explore module-based induction in Dafny for stable, maintainable proofs about inductive data structures. Enhance proof development with Coq-like principles.

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

VMC: A Dafny Library for Verified Monte Carlo Algorithms

Explore VMC, an open-source Dafny library for verified Monte Carlo algorithms, featuring proven samplers for standard distributions usable in Dafny, C#, and Java.

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

Dafny Test Generation - Automated Testing for Verified Programs

Explore automated testing of Dafny programs with DTest. Learn to generate system-level tests, identify dead code, and ensure verified properties hold at runtime, enhancing confidence in code execution.

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