Portfolio Solving for Dafny

Explore portfolio solving for Dafny in this 18-minute conference talk from ACM SIGPLAN. Delve into the concept of brittleness in verification and learn how using multiple SMT solvers can mitigate proof brittleness and enhance verification performance. Discover the benefits of cloud implementation for multi-developer team consistency. Examine potential challenges such as soundness concerns, energy use, and network congestion, along with strategies to address them. Gain insights into why portfolio solving is considered the optimal default for many Dafny use cases, particularly in large codebases with multiple developers. Join speakers Eric Mugnier, Sean McLaughlin, and Aaron Tomb as they present their findings and recommendations for improving the verification process in Dafny.

[Dafny'24] Portfolio Solving for Dafny