The best way to contact me is by email:
This paper provides an experience report of using the Dafny program verifier, at the VerifyThis 2021 program verification competition. The competition aims to evaluate the usability of logic-based program verification tools in a controlled experiment, challenging both the verification tools and the users of those tools. We present the two challenges that we tackled during the competition and discuss our solutions. As a result, we identify strengths and weaknesses of Dafny in the verification of relatively complex algorithms, and report on our experience of applying Dafny in this setting.
We formalize a fragment of the theory of institutions sufficient to establish basic facts about the institution for Event-B, and its relationship with the institution FOPEQ for first-order predicate logic. We prove the satisfaction condition for EVT and encode the institution comorphism FOPEQ → EVT embedding FOPEQ in EVT.