Time bounds for general function pointers

DOI10.1016/J.ENTCS.2012.08.010zbMATH Open1342.68080OpenAlexW2035313585WikidataQ113318083 ScholiaQ113318083MaRDI QIDQ3178280FDOQ3178280

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

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

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)

Cites Work

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

Cited In (2)

• Hoare logics for time bounds. A study in meta theory
• A local-time-induced unique pointer basis

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)