Time Bounds for General Function Pointers

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

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)

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 (1)

• 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)