Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a conference presentation introducing Metamorph, a novel synthesis tool that generates sequences of method calls to construct complex objects satisfying formal specifications in the Dafny programming language. Learn how this innovative approach addresses the computational challenges of synthesizing long sequences of API calls by using counterexamples from the Dafny verifier to reason about method effects incrementally, rather than analyzing entire sequences simultaneously. Discover the tool's two key distance metrics for guiding synthesis, including a piecewise distance metric that provides provably correct lower bounds on solution length and enables framing synthesis as weighted A* search. Understand how the piecewise distance computation treats object states as conjunctions of atomic constraints, identifies which constraints each method call can satisfy, and combines this information through integer programming. Examine evaluation results demonstrating Metamorph's capability to construct programs requiring up to 57 method calls across six benchmark data structures including linked lists, queues, arrays, binary trees, and graphs. See how integration with DTest, Dafny's automated test generation toolkit, enables synthesis of test inputs for parts of the AWS Cryptographic Material Providers Library that were previously uncoverable, and learn about applications extending to executable bytecode generation for virtual machines, showcasing the broader applicability of specification-guided synthesis techniques.
