Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-11737-9_18 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Logical consequence,Abstraction,Computer science,Hoare logic,Usability,Theoretical computer science,Mathematical proof,Temporal logic,Logical framework,Higher-order logic | Conference | 8829 |
ISSN | Citations | PageRank |
0302-9743 | 5 | 0.40 |
References | Authors | |
27 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ton Chanh Le | 1 | 23 | 2.69 |
| Cristian Gherghina | 2 | 85 | 6.60 |
| Aquinas Hobor | 3 | 243 | 17.42 |
| Wei-Ngan Chin | 4 | 868 | 63.37 |