A theory of indirection via approximation

DOI10.1145/1706299.1706322MaRDI QIDQ5255071zbMATH OpenOpenAlexFDO

Authors Aquinas Hobor, Robert Dockins, Andrew W. Appel

Publication date 11 June 2015

Published in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1706299.1706322

zbMATH Keywords

indirection theorystep-indexed models

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 3936482
• A Simple Model of Separation Logic for Higher-Order Store
• Step-indexed Kripke model of separation logic for storable locks
• Semantical analysis of specification logic. II
• Model checking for symbolic-heap separation logic with inductive predicates

Cited in

(8)

• VST-Floyd: a separation logic tool to verify correctness of C programs
• Transfinite step-indexing: decoupling concrete and logical steps
• Verified software toolchain (invited talk)
• Barriers in Concurrent Separation Logic
• Time bounds for general function pointers
• scientific article; zbMATH DE number 3936482 (Why is no real title available?)
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Bringing Order to the Separation Logic Jungle

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A theory of indirection via approximation

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