| Autor: |
Aleksandar Chakarov, Aleksandr Fedchin, Zvonimir Rakamarić, Neha Rungta |
| Rok vydání: |
2022 |
| Zdroj: |
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995232 |
| DOI: |
10.1007/978-3-030-99524-9_23 |
| Popis: |
Dafny is a verification-aware programming language used at Amazon Web Services to develop critical components of their access management, storage, and cryptography infrastructures. The Dafny toolchain provides a verifier that can prove an implementation of a method satisfies its specification. When the underlying SMT solver cannot establish a proof, it generates a counterexample. These counterexamples are hard to understand and their interpretation is often a bottleneck in the proof debugging process. In this paper, we introduce an open-source tool that transforms counterexamples generated by the SMT solver to a more user-friendly format that maps to the Dafny syntax and is suitable for further processing. This new tool allows the Dafny developers to quickly identify the root cause of a problem with their proof, thereby speeding up the development of Dafny projects. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
