ACM SIGPLAN Courses

Improving the Stability of Type Safety Proofs in Dafny

Enhance type soundness proof stability in Dafny using a structured method, demonstrated through a case study and applied to the Cedar language.

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

Caesar: A Verifier for Probabilistic Programs - Dafny'24

Explore Caesar, a verifier for probabilistic programs, featuring an intermediate verification language and real-valued logic for quantitative property verification in programming.

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

Portfolio Solving for Dafny

Mitigate proof brittleness and enhance verification performance using multiple SMT solvers, improving consistency for multi-developer teams in Dafny.

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

Learn 'em Dafny - Incorporating Verification Tools in Software Engineering Education

Explore verification tools like Dafny for software engineering, focusing on building correct systems and understanding formal methods for future professional applications.

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

Randomised Testing of the Dafny Compiler

Explore randomised testing techniques for the Dafny compiler, uncovering miscompilation bugs and failures through innovative tools like fuzz-d and DafnyFuzz.

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

Generation of Verified Assembly Code Using Dafny and Reinforcement Learning

Explore verified assembly code generation using Dafny and reinforcement learning, combining efficiency with automatic correctness verification for complex programming tasks.

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

Colouring Flags with Dafny and Idris - Dafny'24

Explore fine-grained reasoning in Dafny and Idris through the Dutch National Flag problem, comparing their verification approaches and programming paradigms.

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

Measuring Configuration in Code - Risk Assessment and Metrics

Explore techniques for assessing configuration impact on code, including propagating complexity metrics and test coverage to configuration level, to mitigate outage risks and improve system reliability.

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

Evolving a Configuration Language at Google Scale

Explore Google's journey in evolving GCL, an internal configuration language, overcoming challenges of scale and compatibility while implementing gradual improvements and migration strategies.

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

Configuration Testing for Borg at Google

Explore Google's innovative approach to unit testing Borg deployment configurations, addressing complexity challenges in large-scale systems and improving development efficiency.

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

Yes, Configuring is Good, But Have You Ever Tried Justifying? - Extending Justification Diagrams for Configuration Choices

Explore how justification diagrams can enhance configuration choices in complex systems, extending their operational support for decision-making processes.

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

Transpiling Slang Methods to C Functions: An Example of Static Polymorphism for Smalltalk VM Objects

Explore static polymorphism in Slang for transpiling Smalltalk VM objects to C functions. Learn about challenges, benefits, and future enhancements in VM development.

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

Approximating Type Stability in the Julia JIT

Explore an algorithm for approximating type stability in Julia's JIT compiler, enhancing performance in this dynamic scientific computing language.

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

Mixed and Verified Consistency with Propel and ConOpY

Explore mixed consistency in distributed systems using ConOpY language and Propel type system for verifying CRDTs, enhancing data replication and local-first applications.

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

From Static to Dynamic Access Control Policies via Attribute-Based Category Mining

Explore attribute-based category mining for dynamic access control policies, transitioning from static approaches in cybersecurity.

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