Coinductive Verification of Program
Optimizations using Similarity Relations
Sabine Glesner, Johannes Leitner, and Jan Olaf Blech
Technical University of Berlin, Germany
Formal verification methods have gained increased importance due to
their ability to guarantee system correctness and improve reliability.
Nevertheless, the question how proofs are to be formalized in theorem
provers is far from being trivial, yet very important as one needs to
spend much more time on verification if the
formalization was not cleverly chosen. In this paper, we develop and
compare two different possibilities to express coinductive proofs in
the theorem prover Isabelle/HOL. Coinduction is a proof method that
allows for the verification of properties of also non-terminating
state-transition systems. Since coinduction is not as widely used as
other proof techniques as e.g. induction, there are much fewer
"recipes" available how to formalize corresponding proofs and there
are also fewer proof strategies implemented in theorem provers for
coinduction. In this paper, we investigate formalizations for
coinductive proofs of properties on state transition sequences. In
particular, we compare two different possibilities for their
formalization and show their equivalence. The first of these two
formalizations captures the mathematical intuition, while the second
can be used more easily in a theorem prover. We have formally verified
the equivalence of these criteria in Isabelle/HOL, thus establishing a
coalgebraic verification framework. To demonstrate that our
verification framework is suitable for the verification of compiler
optimizations, we have introduced three different, rather
simple transformations that capture typical problems in the
verification of optimizing compilers, even for non-terminating source
programs.