Sciweavers

Share
CADE
2007
Springer

A Termination Checker for Isabelle Hoare Logic

12 years 7 days ago
A Termination Checker for Isabelle Hoare Logic
Abstract. Hoare logic is widely used for software specification and verification. Frequently we need to prove the total correctness of a program: to prove that the program not only satisfies its pre- and post-conditions but also terminates. We have implemented a termination checker for Isabelle's Hoare logic. The tool can be used as an oracle, where Isabelle accepts its claim of termination. The tool can also be used as an Isabelle method for proving the entire total correctness specification. For many loop structures, verifying the tool's termination claim within Isabelle is essentially automatic.
Jia Meng, Lawrence C. Paulson, Gerwin Klein
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Jia Meng, Lawrence C. Paulson, Gerwin Klein
Comments (0)
books