Abstract
This paper shows that an SMT-based program verifier can support reasoning about co-induction-handling infinite data structures, lazy function calls, and user-defined properties defined as greatest fix-points, as well as letting users write co-inductive proofs. Moreover, the support can be packaged to provide a simple user experience. The paper describes the features for co-induction in the language and verifier Dafny, defines their translation into input for a first-order SMT solver, and reports on some encouraging initial experience. © 2014 Springer International Publishing Switzerland.
Cite
CITATION STYLE
Leino, K. R. M., & Moskal, M. (2014). Co-induction simply automatic co-inductive proofs in a program verifier. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8442 LNCS, pp. 382–398). Springer Verlag. https://doi.org/10.1007/978-3-319-06410-9_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
