ACM SIGPLAN Courses

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

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