Encoding Induction Proof in Dafny

Formal verification plays an important role in proving the correctness of safety-critical systems such as cache coherence protocols and security protocols. However, it usually involves rather complicated proofs which demand profound techniques in theorem proving. These techniques are too hard for those programmers with no experience in formal verification to grasp. The induction proof is a good way to reason about the properties of systems. Our work proposes a feasible approach to encode induction proof in Dafny which helps programmers to verify the systems. First, we revisit induction proof and proof dependency. Then, we decompose the complicated proof obligation into induction proof and encode the proof dependency into Dafny. Finally, we present case studies in cache coherence protocols, loop invariants and security protocols to illustrate our approach.