On the public citation graph

Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities

https://doi.org/10.1145/3527318
0 signed · 62 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.
Claim with ORCID
Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/3-540-48749-2_2openalex-snapshot
Protection in Programming-Language Translations
inferredcites →https://doi.org/10.1007/978-3-030-99336-8_7openalex-snapshot
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture
inferredcites →https://doi.org/10.1007/978-3-319-89722-6_4openalex-snapshot
The Meaning of Memory Safety
inferredcites →https://doi.org/10.1007/978-3-319-89884-1_17openalex-snapshot
Reasoning About a Machine with Local Capabilities
inferredcites →https://doi.org/10.1007/978-3-662-54434-1_26openalex-snapshot
The Essence of Higher-Order Concurrent Separation Logic
inferredcites →https://doi.org/10.1007/s10817-009-9155-4openalex-snapshot
A Formally Verified Compiler Back-end
inferredcites →https://doi.org/10.1016/c2013-0-01290-xopenalex-snapshot
Capability-Based Computer Systems
inferredcites →https://doi.org/10.1017/s0956796818000151openalex-snapshot
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
inferredcites →https://doi.org/10.1017/s0956796821000022openalex-snapshot
Linear capabilities for fully abstract compilation of separation-logic-verified code
inferredcites →https://doi.org/10.1109/csf.2019.00024openalex-snapshot
Temporal Safety for Stack Allocated Memory on Capability Machines
inferredcites →https://doi.org/10.1109/csf51468.2021.00036openalex-snapshot
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle
inferredcites →https://doi.org/10.1109/eurosp.2016.22openalex-snapshot
Reasoning about Object Capabilities with Logical Relations and Effect Parametricity
inferredcites →https://doi.org/10.1109/sp.2013.13openalex-snapshot
SoK: Eternal War in Memory
inferredcites →https://doi.org/10.1109/sp.2015.55openalex-snapshot
Micro-Policies: Formally Verified, Tag-Based Security Monitors
inferredcites →https://doi.org/10.1109/sp.2015.9openalex-snapshot
CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization
inferredcites →https://doi.org/10.1109/sp.2018.00066openalex-snapshot
Protecting the Stack with Metadata Policies and Tagged Hardware
inferredcites →https://doi.org/10.1109/sp40000.2020.00055openalex-snapshot
Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process
inferredcites →https://doi.org/10.1109/tc.2019.2914037openalex-snapshot
CHERI Concentrate: Practical Compressed Capabilities
inferredcites →https://doi.org/10.1145/1284320.1284325openalex-snapshot
A bisimulation for type abstraction and recursion
inferredcites →https://doi.org/10.1145/1480881.1480925openalex-snapshot
State-dependent representation independence
inferredcites →https://doi.org/10.1145/168619.168635openalex-snapshot
Efficient software-based fault isolation
inferredcites →https://doi.org/10.1145/1706299.1706323openalex-snapshot
A relational modal logic for higher-order stateful ADTs
inferredcites →https://doi.org/10.1145/1863543.1863566openalex-snapshot
The impact of higher-order state and control effects on local relational reasoning
inferredcites →https://doi.org/10.1145/1926385.1926401openalex-snapshot
Step-indexed kripke models over recursive worlds
inferredcites →https://doi.org/10.1145/195473.195579openalex-snapshot
Hardware support for fast capability-based addressing
inferredcites →https://doi.org/10.1145/2500365.2500600openalex-snapshot
Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
inferredcites →https://doi.org/10.1145/2535838.2535839openalex-snapshot
A verified information-flow architecture
inferredcites →https://doi.org/10.1145/2676726.2676980openalex-snapshot
Iris
inferredcites →https://doi.org/10.1145/2951913.2951943openalex-snapshot
Higher-order ghost state
inferredcites →https://doi.org/10.1145/3009837.3009855openalex-snapshot
Interactive proofs in higher-order concurrent separation logic
inferredcites →https://doi.org/10.1145/3009837.3009877openalex-snapshot
A relational model of types-and-effects in higher-order concurrent separation logic
inferredcites →https://doi.org/10.1145/3133913openalex-snapshot
Robust and compositional verification of object capability patterns
inferredcites →https://doi.org/10.1145/3209108.3209174openalex-snapshot
ReLoC
inferredcites →https://doi.org/10.1145/3236772openalex-snapshot
MoSeL: a general, extensible modal framework for interactive proofs in separation logic
inferredcites →https://doi.org/10.1145/3243734.3243745openalex-snapshot
When Good Components Go Bad
inferredcites →https://doi.org/10.1145/3280984openalex-snapshot
Formal Approaches to Secure Compilation
inferredcites →https://doi.org/10.1145/3290332openalex-snapshot
StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
inferredcites →https://doi.org/10.1145/3352460.3358288openalex-snapshot
CHERIvoke
inferredcites →https://doi.org/10.1145/3363519openalex-snapshot
Reasoning about a Machine with Local Capabilities
inferredcites →https://doi.org/10.1145/3434287openalex-snapshot
Efficient and provable local capability revocation using uninitialized capabilities
inferredcites →https://doi.org/10.1145/3527318openalex-snapshot
Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities
inferredcites →https://doi.org/10.1145/365230.365252openalex-snapshot
Programming semantics for multiprogrammed computations
inferredcites →https://doi.org/10.48456/tr-907openalex-snapshot
Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 6)
inferredcites →https://doi.org/10.48456/tr-951openalex-snapshot
Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8)
inferredcites →https://doi.org/10.5281/zenodo.5821861openalex-snapshot
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities (Artifact)

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.1109/csf57540.2023.00029openalex-snapshot
A Generic Framework to Develop and Verify Security Mechanisms at the Microarchitectural Level: Application to Control-Flow Integrity
inferred← citeshttps://doi.org/10.1109/csf57540.2023.00037openalex-snapshot
Formalizing Stack Safety as a Security Property
inferred← citeshttps://doi.org/10.1145/3586043openalex-snapshot
Proof Automation for Linearizability in Separation Logic
inferred← citeshttps://doi.org/10.1145/3591265openalex-snapshot
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
inferred← citeshttps://doi.org/10.1145/3591279openalex-snapshot
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A
inferred← citeshttps://doi.org/10.1145/3623510openalex-snapshot
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code
inferred← citeshttps://doi.org/10.1145/3632851openalex-snapshot
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
inferred← citeshttps://doi.org/10.1145/3632868openalex-snapshot
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
inferred← citeshttps://doi.org/10.1145/3658644.3670288openalex-snapshot
SECOMP: Formally Secure Compilation of Compartmentalized C Programs
inferred← citeshttps://doi.org/10.1145/3689722openalex-snapshot
Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly
inferred← citeshttps://doi.org/10.1145/3703595.3705878openalex-snapshot
A CHERI C Memory Model for Verified Temporal Safety
inferred← citeshttps://doi.org/10.1145/3719027.3744801openalex-snapshot
Logical Relations for Formally Verified Authenticated Data Structures
inferred← citeshttps://doi.org/10.1145/3729329openalex-snapshot
Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture
inferred← citeshttps://doi.org/10.1145/3731569.3764844openalex-snapshot
CHERIoT RTOS: An OS for Fine-Grained Memory-Safe Compartments on Low-Cost Embedded Devices
inferred← citeshttps://doi.org/10.1145/3808287openalex-snapshot
Cerisier: A Program Logic for Attestation in a Capability Machine
inferred← citeshttps://doi.org/10.70675/8640ad41zfb4fz40ecz8e27z200801a72369openalex-snapshot
Formal Specification and Verification of Security Mechanisms for RISC-V Processors
showing the first 16 of 17 · page through all 17
Editorial review for independent work. ICSAC — the Institute for Complexity Science and Advanced Computing — runs a structured editorial panel for researchers publishing outside journals, and publishes on CiteStamp rails. Submission is free and goes through ORCID: icsacinstitute.org/submit.