2025
Three ways of proving termination of loops
Publication
Publication
We investigate three proof rules for proving termination of while programs and show their proof-theoretic equivalence. This involves a proof-theoretic analysis of various auxiliary proof rules in Hoare’s logic. By discussing representations of proofs in the form of proof outlines, we reveal differences between these equivalent proof rules when used in practice. We also address applications in the context of the paradigm of design by contract.
| Additional Metadata | |
|---|---|
| doi.org/10.1007/978-3-031-73887-6_19 | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
Apt, K., de Boer, F., & Olderog, E.-R. (2025). Three ways of proving termination of loops. In The Combined Power of Research, Education, and Dissemination (pp. 280–301). doi:10.1007/978-3-031-73887-6_19 |
|
