On the public citation graph

TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

https://doi.org/10.1145/3477082
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/11817949_16openalex-snapshot
A New Type System for Deadlock-Free Processes
inferredcites →https://doi.org/10.1007/3-540-44929-9_27openalex-snapshot
Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness
inferredcites →https://doi.org/10.1007/978-3-319-71237-6_14openalex-snapshot
Safety and Liveness of MCS Lock—Layer by Layer
inferredcites →https://doi.org/10.1007/978-3-319-89884-1_15openalex-snapshot
Deadlock-Free Monitors
inferredcites →https://doi.org/10.1007/978-3-540-28644-8_2openalex-snapshot
A Semantics for Concurrent Separation Logic
inferredcites →https://doi.org/10.1007/978-3-540-28644-8_4openalex-snapshot
Resources, Concurrency and Local Reasoning
inferredcites →https://doi.org/10.1007/978-3-642-00590-9_26openalex-snapshot
Deny-Guarantee Reasoning
inferredcites →https://doi.org/10.1007/978-3-642-11957-6_22openalex-snapshot
Deadlock-Free Channels and Locks
inferredcites →https://doi.org/10.1007/978-3-642-14107-2_24openalex-snapshot
Concurrent Abstract Predicates
inferredcites →https://doi.org/10.1007/978-3-642-22012-8_36openalex-snapshot
Liveness-Preserving Atomicity Abstraction
inferredcites →https://doi.org/10.1007/978-3-642-25873-2_22openalex-snapshot
On the Nature of Progress
inferredcites →https://doi.org/10.1007/978-3-642-40184-8_17openalex-snapshot
Characterizing Progress Properties of Concurrent Objects via Contextual Refinements
inferredcites →https://doi.org/10.1007/978-3-642-54833-8_16openalex-snapshot
Communicating State Transition Systems for Fine-Grained Concurrent Resources
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/978-3-662-49498-1_8openalex-snapshot
Modular Termination Verification for Non-blocking Concurrency
inferredcites →https://doi.org/10.1007/978-3-662-54434-1_34openalex-snapshot
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
inferredcites →https://doi.org/10.1007/bfb0015261openalex-snapshot
Alternating automata and program verification
inferredcites →https://doi.org/10.1016/j.entcs.2005.11.059openalex-snapshot
Variables as Resource in Separation Logic
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.2013.18openalex-snapshot
Quantitative Reasoning for Proving Lock-Freedom
inferredcites →https://doi.org/10.1145/1146381.1146382openalex-snapshot
The art of multiprocessor programming
inferredcites →https://doi.org/10.1145/1273442.1250771openalex-snapshot
Proving thread termination
inferredcites →https://doi.org/10.1145/1480881.1480886openalex-snapshot
Proving that non-blocking algorithms don't block
inferredcites →https://doi.org/10.1145/1594834.1480886openalex-snapshot
Proving that non-blocking algorithms don't block
inferredcites →https://doi.org/10.1145/2480359.2429104openalex-snapshot
Views
inferredcites →https://doi.org/10.1145/2480359.2429134openalex-snapshot
Subjective auxiliary state for coarse-grained concurrency
inferredcites →https://doi.org/10.1145/2603088.2603123openalex-snapshot
Compositional verification of termination-preserving refinement of concurrent programs
inferredcites →https://doi.org/10.1145/2676726.2676980openalex-snapshot
Iris
inferredcites →https://doi.org/10.1145/2775051.2676980openalex-snapshot
Iris
inferredcites →https://doi.org/10.1145/2837614.2837635openalex-snapshot
A program logic for concurrent objects under fair scheduling
inferredcites →https://doi.org/10.1145/2914770.2837635openalex-snapshot
A program logic for concurrent objects under fair scheduling
inferredcites →https://doi.org/10.1145/3158108openalex-snapshot
Progress of concurrent objects with partial methods
inferredcites →https://doi.org/10.1145/3210258openalex-snapshot
Modular Termination Verification of Single-Threaded and Multithreaded Programs
inferredcites →https://doi.org/10.1145/3290378openalex-snapshot
Iron: managing obligations in higher-order concurrent separation logic
inferredcites →https://doi.org/10.1145/3296979.3192381openalex-snapshot
Certified concurrent abstraction layers
inferredcites →https://doi.org/10.1145/3477082openalex-snapshot
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
inferredcites →https://doi.org/10.1145/357172.357178openalex-snapshot
Proving Liveness Properties of Concurrent Programs
inferredcites →https://doi.org/10.1145/78969.78972openalex-snapshot
Linearizability: a correctness condition for concurrent objects
inferredcites →https://doi.org/10.25560/47923openalex-snapshot
Reasoning with time and data abstractions
inferredcites →https://doi.org/10.3929/ethz-a-010341095openalex-snapshot
Modular Verification of Finite Blocking in Non-terminating Programs
inferredcites →https://doi.org/10.4230/lipics.ecoop.2018.4openalex-snapshot
A Concurrent Specification of POSIX File Systems
inferredcites →https://doi.org/10.4230/lipics.ecoop.2019.19openalex-snapshot
Transferring Obligations Through Synchronizations
inferredcites →https://doi.org/10.5555/1883978.1884012openalex-snapshot
Concurrent abstract predicates

What points at this work

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

inferred← citeshttps://doi.org/10.1007/978-3-030-61362-4_29openalex-snapshot
Modular Verification of Liveness Properties of the I/O Behavior of Imperative Programs
inferred← citeshttps://doi.org/10.1007/978-3-030-90870-6_22openalex-snapshot
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA
inferred← citeshttps://doi.org/10.1007/978-3-031-66676-6_4openalex-snapshot
Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures
inferred← citeshttps://doi.org/10.1007/978-3-032-26204-2_6openalex-snapshot
Towards Proving Liveness on Weak Memory
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/3453483.3454031openalex-snapshot
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic
inferred← citeshttps://doi.org/10.1145/3571229openalex-snapshot
Higher-Order Leak and Deadlock Free Locks
inferred← citeshttps://doi.org/10.1145/3591253openalex-snapshot
Fair Operational Semantics
inferred← citeshttps://doi.org/10.1145/3632889openalex-snapshot
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
inferred← citeshttps://doi.org/10.1145/3689720openalex-snapshot
Non-termination Proving at Scale
inferred← citeshttps://doi.org/10.1145/3720525openalex-snapshot
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
inferred← citeshttps://doi.org/10.1145/3729284openalex-snapshot
Destabilizing Iris
inferred← citeshttps://doi.org/10.1145/3763091openalex-snapshot
Structural Temporal Logic for Mechanized Program Verification
inferred← citeshttps://doi.org/10.1145/3798240openalex-snapshot
Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic
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.2010.07080openalex-snapshot
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper)
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.