Dafny Meets the Verification Benchmarks Challenge

A suite of verification benchmarks for software verification tools and techniques, presented at VSTTE 2008 [11], provides an initial catalogue of benchmark challenges for the Verified Software Initiative. This paper presents solutions to these eight benchmarks using the language and verifier Dafny. A Dafny program includes specifications, code, inductive invariants, and termination metrics. Each of the eight programs is fed to the Dafny verifier, which without further user interaction automatically performs the verification in a few seconds. 0 The Challenge The motivation from this work comes from the Verified Software Initiative [3] and the suite of eight purposefully designed, incremental benchmarks for tools and techniques to prove total correctness of sequential object-based and object-oriented software, as presented by Weide et al. at VSTTE 2008 [11]. A solution to part of the first benchmark is provided, while the main contribution of their paper is the provision of a benchmark s...

• Type: Journal
• Year: 2010
• Where: VSTTE
• Authors: K. Rustan M. Leino, Rosemary Monahan
• Keywords: Dafny Programs, Software Engineering, Verified Software Initiative, Verifier Dafny, VSTTE 2010