License
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.10351.3
URN: urn:nbn:de:0030-drops-28050
URL: https://drops.dagstuhl.de/opus/volltexte/2010/2805/
|
Go to the corresponding Portal |
Dockins, Robert ;
Hobor, Aquinas
A Theory of Termination via Indirection
Abstract
Step-indexed models provide approximations to a class of domain
equations and can prove type safety, partial correctness, and program
equivalence; however, a common misconception is that they
are inapplicable to liveness problems. We disprove this by applying
step-indexing to develop the first Hoare logic of total correctness
for a language with function pointers and semantic assertions.
In fact, from a liveness perspective, our logic is stronger: we verify
explicit time resource bounds. We apply our logic to examples containing
nontrivial "higher-order" uses of function pointers and we
prove soundness with respect to a standard operational semantics.
Our core technique is very compact and may be applicable to other
liveness problems. Our results are machine checked in Coq.
BibTeX - Entry
@InProceedings{dockins_et_al:DagSemProc.10351.3,
author = {Dockins, Robert and Hobor, Aquinas},
title = {{A Theory of Termination via Indirection}},
booktitle = {Modelling, Controlling and Reasoning About State},
pages = {1--12},
series = {Dagstuhl Seminar Proceedings (DagSemProc)},
ISSN = {1862-4405},
year = {2010},
volume = {10351},
editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2010/2805},
URN = {urn:nbn:de:0030-drops-28050},
doi = {10.4230/DagSemProc.10351.3},
annote = {Keywords: Step-indexed Models, Termination}
}
|
Keywords: |
|
Step-indexed Models, Termination |
|
Collection: |
|
10351 - Modelling, Controlling and Reasoning About State |
|
Issue Date: |
|
2010 |
|
Date of publication: |
|
04.11.2010 |
