Please use this identifier to cite or link to this item: https://doi.org/10.1016/j.entcs.2012.08.010
Title: Time bounds for general function pointers
Authors: Dockins, R.
Hobor, A. 
Keywords: Step-indexed models
Termination
Issue Date: 24-Sep-2012
Source: Dockins, R., Hobor, A. (2012-09-24). Time bounds for general function pointers. Electronic Notes in Theoretical Computer Science 286 : 139-155. ScholarBank@NUS Repository. https://doi.org/10.1016/j.entcs.2012.08.010
Abstract: We develop a logic of explicit time resource bounds for a language with function pointers and semantic assertions. 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 resource bounding problems, and is the first application of stepindexed models in which the outermost quantifier is existential instead of universal. Our results are machine checked in Coq. © 2012 Elsevier B.V.
Source Title: Electronic Notes in Theoretical Computer Science
URI: http://scholarbank.nus.edu.sg/handle/10635/78392
ISSN: 15710661
DOI: 10.1016/j.entcs.2012.08.010
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

18
checked on Mar 9, 2018

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.