A Theory of Termination via Indirection

Authors Robert Dockins, Aquinas Hobor



PDF
Thumbnail PDF

File

DagSemProc.10351.3.pdf
  • Filesize: 165 kB
  • 12 pages

Document Identifiers

Author Details

Robert Dockins
Aquinas Hobor

Cite As Get BibTex

Robert Dockins and Aquinas Hobor. A Theory of Termination via Indirection. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/DagSemProc.10351.3

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.

Subject Classification

Keywords
  • Step-indexed Models
  • Termination

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail