On the public citation graph

The future is ours: prophecy variables in separation logic

https://doi.org/10.1145/3371113
0 signed · 96 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-36108-1_18openalex-snapshot
A Practical Multi-word Compare-and-Swap Operation
inferredcites →https://doi.org/10.1007/3-540-44898-5_4openalex-snapshot
Checking Interference with Fractional Permissions
inferredcites →https://doi.org/10.1007/978-3-319-89884-1_32openalex-snapshot
Paxos Consensus, Deconstructed and Abstracted
inferredcites →https://doi.org/10.1007/978-3-540-74407-8_18openalex-snapshot
A Marriage of Rely/Guarantee and Separation Logic
inferredcites →https://doi.org/10.1007/978-3-642-15375-4_27openalex-snapshot
Reasoning about Optimistic Concurrency Using a Program Logic for History
inferredcites →https://doi.org/10.1007/978-3-642-20398-5_4openalex-snapshot
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java
inferredcites →https://doi.org/10.1007/978-3-642-29952-0_12openalex-snapshot
A Structural Approach to Prophecy Variables
inferredcites →https://doi.org/10.1007/978-3-662-44202-9_9openalex-snapshot
TaDA: A Logic for Time and Data Abstraction
inferredcites →https://doi.org/10.1007/978-3-662-46669-8_14openalex-snapshot
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
inferredcites →https://doi.org/10.1007/bf00268134openalex-snapshot
An axiomatic proof technique for parallel programs I
inferredcites →https://doi.org/10.1016/0304-3975(91)90224-popenalex-snapshot
The existence of refinement mappings
inferredcites →https://doi.org/10.1016/j.tcs.2006.12.035openalex-snapshot
Resources, concurrency, and local reasoning
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.1109/lics.1988.5115openalex-snapshot
The existence of refinement mappings
inferredcites →https://doi.org/10.1109/lics.2002.1029817openalex-snapshot
Separation logic: a logic for shared mutable data structures
inferredcites →https://doi.org/10.1145/1925844.1926417openalex-snapshot
Expressive modular fine-grained concurrency specification
inferredcites →https://doi.org/10.1145/1925844.1926431openalex-snapshot
Making prophecies with decision predicates
inferredcites →https://doi.org/10.1145/1926385.1926431openalex-snapshot
Making prophecies with decision predicates
inferredcites →https://doi.org/10.1145/2429069.2429104openalex-snapshot
Views
inferredcites →https://doi.org/10.1145/2429069.2429111openalex-snapshot
Logical relations for fine-grained concurrency
inferredcites →https://doi.org/10.1145/2429069.2429134openalex-snapshot
Subjective auxiliary state for coarse-grained concurrency
inferredcites →https://doi.org/10.1145/2480359.2429134openalex-snapshot
Subjective auxiliary state for coarse-grained concurrency
inferredcites →https://doi.org/10.1145/2491956.2462189openalex-snapshot
Modular verification of linearizability with non-fixed linearization points
inferredcites →https://doi.org/10.1145/2660193.2660243openalex-snapshot
GPS
inferredcites →https://doi.org/10.1145/2676726.2676980openalex-snapshot
Iris
inferredcites →https://doi.org/10.1145/3009837.3009855openalex-snapshot
Interactive proofs in higher-order concurrent separation logic
inferredcites →https://doi.org/10.1145/3093333.3009855openalex-snapshot
Interactive proofs in higher-order concurrent separation logic
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/3340672.3341118openalex-snapshot
Specifying I/O using abstract nested hoare triples in separation logic
inferredcites →https://doi.org/10.1145/3371101openalex-snapshot
Spy game: verifying a local generic solver in Iris
inferredcites →https://doi.org/10.1145/361227.361234openalex-snapshot
Reduction
inferredcites →https://doi.org/10.1145/78969.78972openalex-snapshot
Linearizability: a correctness condition for concurrent objects
inferredcites →https://doi.org/10.4230/lipics.ecoop.2017.8openalex-snapshot
Concurrent Data Structures Linked in Time
inferredcites →https://doi.org/10.5281/zenodo.3541917openalex-snapshot
The Future is Ours: Prophecy Variables in Separation Logic -- Artifact

What points at this work

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

inferred← backgroundhttps://doi.org/10.5281/zenodo.3570660zenodo-depositor-declared
inferred← citeshttps://doi.org/10.1007/978-3-030-44914-8_18openalex-snapshot
RustHorn: CHC-Based Verification for Rust Programs
inferred← citeshttps://doi.org/10.1007/978-3-031-21037-2_4openalex-snapshot
RHLE: Modular Deductive Verification of Relational $$\forall \exists $$ Properties
inferred← citeshttps://doi.org/10.1007/978-3-031-50521-8_11openalex-snapshot
Borrowable Fractional Ownership Types for Verification
inferred← citeshttps://doi.org/10.1007/978-3-031-98668-0_4openalex-snapshot
Raven: An SMT-Based Concurrency Verifier
inferred← citeshttps://doi.org/10.1007/978-3-032-26204-2_19openalex-snapshot
RustyDL: A Program Logic for Rust
inferred← citeshttps://doi.org/10.1109/csf54842.2022.9919658openalex-snapshot
Prophecy Variables for Hyperproperty Verification
inferred← citeshttps://doi.org/10.1145/3371101openalex-snapshot
Spy game: verifying a local generic solver in Iris
inferred← citeshttps://doi.org/10.1145/3385412.3386029openalex-snapshot
Verifying concurrent search structure templates
inferred← citeshttps://doi.org/10.1145/3427761.3428345openalex-snapshot
A separation logic to verify termination of busy-waiting for abrupt program exit
inferred← citeshttps://doi.org/10.1145/3428196openalex-snapshot
Proving highly-concurrent traversals correct
inferred← citeshttps://doi.org/10.1145/3434286openalex-snapshot
On algebraic abstractions for concurrent separation logics
inferred← citeshttps://doi.org/10.1145/3437992.3439930openalex-snapshot
Contextual refinement of the Michael-Scott queue (proof pearl)
inferred← citeshttps://doi.org/10.1145/3453483.3454036openalex-snapshot
RefinedC: automating the foundational verification of C code with refined ownership types
inferred← citeshttps://doi.org/10.1145/3462205openalex-snapshot
RustHorn: CHC-based Verification for Rust Programs
inferred← citeshttps://doi.org/10.1145/3473571openalex-snapshot
Formal verification of a concurrent bounded queue in a weak memory model
inferred← citeshttps://doi.org/10.1145/3485490openalex-snapshot
Verifying concurrent multicopy search structures
inferred← citeshttps://doi.org/10.1145/3485512openalex-snapshot
A type system for extracting functional specifications from memory-safe imperative programs
inferred← citeshttps://doi.org/10.1145/3492545openalex-snapshot
Prophecy Made Simple
inferred← citeshttps://doi.org/10.1145/3497775.3503689openalex-snapshot
Mechanized verification of a fine-grained concurrent queue from meta’s folly library
inferred← citeshttps://doi.org/10.1145/3498694openalex-snapshot
Visibility reasoning for concurrent snapshot algorithms
inferred← citeshttps://doi.org/10.1145/3519939.3523432openalex-snapshot
Diaframe: automated verification of fine-grained concurrent programs in Iris
inferred← citeshttps://doi.org/10.1145/3519939.3523451openalex-snapshot
Compass: strong and compositional library specifications in relaxed memory separation logic
inferred← citeshttps://doi.org/10.1145/3519939.3523704openalex-snapshot
RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code
inferred← citeshttps://doi.org/10.1145/3547631openalex-snapshot
Later credits: resourceful reasoning for the later modality
inferred← citeshttps://doi.org/10.1145/3563337openalex-snapshot
A concurrent program logic with a future and history
inferred← citeshttps://doi.org/10.1145/3571231openalex-snapshot
A Compositional Theory of Linearizability
inferred← citeshttps://doi.org/10.1145/3586043openalex-snapshot
Proof Automation for Linearizability in Separation Logic
inferred← citeshttps://doi.org/10.1145/3591296openalex-snapshot
Embedding Hindsight Reasoning in Separation Logic
inferred← citeshttps://doi.org/10.1145/3600006.3613172openalex-snapshot
Grove: a Separation-Logic Library for Verifying Distributed Systems
inferred← citeshttps://doi.org/10.1145/3622827openalex-snapshot
Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
inferred← citeshttps://doi.org/10.1145/3632868openalex-snapshot
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
inferred← citeshttps://doi.org/10.1145/3632911openalex-snapshot
VST-A: A Foundationally Sound Annotation Verifier
inferred← citeshttps://doi.org/10.1145/3632924openalex-snapshot
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
inferred← citeshttps://doi.org/10.1145/3636501.3636950openalex-snapshot
Unification for Subformula Linking under Quantifiers
inferred← citeshttps://doi.org/10.1145/3643668openalex-snapshot
A Compositional Theory of Linearizability
inferred← citeshttps://doi.org/10.1145/3649857openalex-snapshot
Scenario-Based Proofs for Concurrent Objects
inferred← citeshttps://doi.org/10.1145/3656384openalex-snapshot
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
inferred← citeshttps://doi.org/10.1145/3676954openalex-snapshot
A Logical Approach to Type Soundness
inferred← citeshttps://doi.org/10.1145/3694906.3743304openalex-snapshot
Formal Machine-Verification of MemSnap: An Efficient, Far-Future Linearizable Snapshot Algorithm
inferred← citeshttps://doi.org/10.1145/3704847openalex-snapshot
Program Logics à la Carte
inferred← citeshttps://doi.org/10.1145/3704894openalex-snapshot
Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning
inferred← citeshttps://doi.org/10.1145/3719027.3744801openalex-snapshot
Logical Relations for Formally Verified Authenticated Data Structures
inferred← citeshttps://doi.org/10.1145/3720492openalex-snapshot
Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
inferred← citeshttps://doi.org/10.1145/3720525openalex-snapshot
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
inferred← citeshttps://doi.org/10.1145/3729246openalex-snapshot
Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
inferred← citeshttps://doi.org/10.1145/3729248openalex-snapshot
Verifying Lock-Free Traversals in Relaxed Memory Separation Logic
inferred← citeshttps://doi.org/10.1145/3729250openalex-snapshot
Nola: Later-Free Ghost State for Verifying Termination in Iris
inferred← citeshttps://doi.org/10.1145/3729333openalex-snapshot
Thrust: A Prophecy-Based Refinement Type System for Rust
inferred← citeshttps://doi.org/10.1145/3747514openalex-snapshot
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
inferred← citeshttps://doi.org/10.1145/3763123openalex-snapshot
Efficient Decrease-and-Conquer Linearizability Monitoring
inferred← citeshttps://doi.org/10.1145/3779031.3779095openalex-snapshot
Building Blocks for Step-Indexed Program Logics
inferred← citeshttps://doi.org/10.1145/3808265openalex-snapshot
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
inferred← citeshttps://doi.org/10.1145/3808337openalex-snapshot
A Verified Parallel Scheduler for OCaml 5
inferred← citeshttps://doi.org/10.1145/3828682openalex-snapshot
Completeness of Iris-Based Program Logics
inferred← citeshttps://doi.org/10.15479/at:ista:8332openalex-snapshot
Verifying concurrent programs: Refinement, synchronization, sequentialization
inferred← citeshttps://doi.org/10.46298/lmcs-17(3:9)2021openalex-snapshot
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
inferred← citeshttps://doi.org/10.46298/lmcs-18(3:26)2022openalex-snapshot
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
inferred← citeshttps://doi.org/10.48550/arxiv.2007.10215openalex-snapshot
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report
inferred← citeshttps://doi.org/10.48550/arxiv.2007.12015openalex-snapshot
Dataflow Analysis With Prophecy and History Variables
inferred← citeshttps://doi.org/10.5281/zenodo.10100891openalex-snapshot
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement - Coq Artifact
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.