A termination checker for isabelle hoare logic

Jia Meng, Lawrence C. Paulson, Gerwin Klein

Research output: Contribution to journalConference articlepeer-review

1 Citation (Scopus)

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.

Original languageEnglish
Pages (from-to)104-118
Number of pages15
JournalCEUR Workshop Proceedings
Volume259
Publication statusPublished - 2007
Externally publishedYes
Event4th International Verification Workshop, VERIFY 2007, Affiliated with the 21st Conference on Automated Deduction, CADE 2007 - Bremen, Germany
Duration: 15 Jul 200716 Jul 2007

Fingerprint

Dive into the research topics of 'A termination checker for isabelle hoare logic'. Together they form a unique fingerprint.

Cite this