Time bounds for general function pointers

DOI10.1016/J.ENTCS.2012.08.010MaRDI QIDQ3178280zbMATHOpenAlexWikidataFDO

Authors Robert Dockins, Aquinas Hobor

Publication date 8 July 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2012.08.010

zbMATH Keywords

terminationstep-indexed models

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Recommendations

• Hoare logics for time bounds. A study in meta theory
• scientific article; zbMATH DE number 4181310
• Bounded Linear Types in a Resource Semiring
• Complexity analysis in presence of control operators and higher-order functions
• Pointer logic for verification of pointer programs

Cites work

• A program logic for resources
• A theory of indirection via approximation
• Descriptive and Relative Completeness of Logics for Higher-Order Functions
• From process logic to program logic
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• State-dependent representation independence
• Step-indexed Kripke models over recursive worlds

Cited in

(3)

• A local-time-induced unique pointer basis
• Time credits and time receipts in Iris
• Hoare logics for time bounds. A study in meta theory

Describes a project that uses

Uses Software

• Coq
• Boogie
• Mechanized Semantic Library

This page was built for publication: Time bounds for general function pointers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3178280)