Advertisement
Published in:
2014 | OriginalPaper | Chapter
A Resource-Based Logic for Termination and Non-termination Proofs
Authors : Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan Chin
Published in: Formal Methods and Software Engineering
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We propose a unified logical framework for specifying and proving
both
termination and non-termination of various programs. Our framework is based on a resource logic which captures both upper
and
lower bounds on resources used by the programs. By an abstraction, we evolve this resource logic for execution length into a temporal logic with three predicates to reason about termination, non-termination or unknown. We introduce a new logical entailment system for temporal constraints and show how Hoare logic can be seamlessly used to prove termination and non-termination in our unified framework. Though this paper’s focus is on the formal foundations for a new unified framework, we also report on the usability and practicality of our approach by specifying and verifying both termination and non-termination properties for about 300 programs, collected from a variety of sources. This adds a modest 5-10% verification overhead when compared to underlying partial-correctness verification system.