@inproceedings{91b5302656ad4fa8b7e228c4cb9b45a8,
title = "Encoding Induction Proof in Dafny",
abstract = "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.",
keywords = "Dafny, Invariant, Proof Dependency, Security, Theorem Proving, loop invariants",
author = "Hongjian Jiang and Yongjian Li and Sijun Tan and Yongxin Zhao",
note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 15th International Symposium on Theoretical Aspects of Software Engineering, TASE 2021 ; Conference date: 25-08-2021 Through 27-08-2021",
year = "2021",
month = aug,
doi = "10.1109/TASE52547.2021.00025",
language = "英语",
series = "Proceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "95--102",
booktitle = "Proceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021",
address = "美国",
}