VMC: A Dafny Library for Verified Monte Carlo Algorithms
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a conference talk introducing VMC, an open-source Dafny library for verified randomized algorithms of the Monte Carlo type. Delve into the library's offerings of verified samplers for standard distributions, applicable in Dafny, C#, and Java code. Examine the three-part structure of each sampler: a functional model transforming bitstreams to distribution domain values, a proof validating the model's distribution, and an imperative implementation using external random bits, proven equivalent to the functional model. Follow a detailed walkthrough of each step using the uniform distribution as an example. Gain insights into the project's current status and potential future developments in the field of verified Monte Carlo algorithms.
Syllabus
[Dafny'24] VMC: a Dafny Library for Verified Monte Carlo Algorithms
Taught by
ACM SIGPLAN
Related Courses
Teaching Logic and Set Theory with DafnyACM SIGPLAN via YouTube CLOVER: Closed-Loop Verifiable Code Generation - Dafny'24
ACM SIGPLAN via YouTube Verifying a Concurrent File System with Sequential Reasoning
ACM SIGPLAN via YouTube Generating Conforming Programs with Xsmith
ACM SIGPLAN via YouTube Domesticating Automation for Large-Scale Verification Systems - Dafny'24
ACM SIGPLAN via YouTube