Reasoning about a machine with local capabilities. Provably safe stack and return pointer management

DOI10.1007/978-3-319-89884-1_17zbMath1418.68067OpenAlexW2796499075MaRDI QIDQ2323991

Lars Birkedal, Dominique Devriese, Lau Skorstengaard

Publication date: 13 September 2019

Full work available at URL: https://doi.org/10.1007/978-3-319-89884-1_17

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Linear capabilities for fully abstract compilation of separation-logic-verified code ⋮ StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

This page was built for publication: Reasoning about a machine with local capabilities. Provably safe stack and return pointer management