A Termination Checker for Isabelle Hoare Logic

Select |




Print


Meng, Jia; Paulson, Lawrence C.; Klein, Gerwin

Meng, Jia; Paulson, Lawrence C.; Klein, Gerwin


2007-07-04


Conference Material


4th International Verification Workshop - VERIFY'07


Bremen, Germany


259


104-118


Hoare logic is widely used for software specification and verification. Frequen tly we need to prove the total correctness of a program: to prove that the progr am 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 spe cification. For many loop structures, verifying the tool's termination claim wit hin Isabelle is essentially automatic.


CEUR Workshop Proceedings


http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-259/


CEUR Workshop Proceedings


1613-0073


1613-0073


nicta:133


Meng, Jia; Paulson, Lawrence C.; Klein, Gerwin. A Termination Checker for Isabelle Hoare Logic. In: Bernhard Beckert Editor, editor/s. 4th International Verification Workshop - VERIFY'07; Bremen, Germany. CEUR Workshop Proceedings; 2007-07-04. 104-118.



Loading citation data...

Citation counts
(Requires subscription to view)