AVL-Tree implemented in Dafny
All proof obligations could be verified successfully. However, it was possible to verify invalid counterexamples. This leads to the assumption that Dafny does currently not completely check multiple predicates.
The project is part of the seminar Deductive Softwareverification at LMU Munich.
Seminar Paper: Object-Oriented Verification with Dafny
Richard Poschinger
Based on the Dafny Binary Tree by Microsoft
Distributed under the MIT license.