Experimental Program Verification in the Theorema System.
Tudor Jebelean, Laura Kovács, Nikolaj Popov · 2004
We describe practical experiments of program verification in the frame of the Theorema system. This includes both imperative programs (using Hoare logic), as well as functional programs (using fixpoint theory). For a certain class of imperative programs we are able to generate automatically the loop invariants and then verification conditions, by using combinatorial and algebraic techniques. Verification conditions for functional recursive programs are derived and soundness theorem is proven. The verification conditions in both cases are generated as natural-style predicate logic formulae, which can be then proven by Theorema, by issuing naturalstyle proofs which are human–readable.