On the public citation graph
Reducing liveness to safety in first-order logic
0 signed · 112 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.
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.
What this work says
Outgoing claims: the papers this work cites, builds on, or argues with.
inferredcites →https://doi.org/10.1007/10722167_26openalex-snapshot
Liveness and Acceleration in Parameterized Verification
inferredcites →https://doi.org/10.1007/11817949_7openalex-snapshot
Proving Liveness by Backwards Reachability
inferredcites →https://doi.org/10.1007/3-540-36377-7_1openalex-snapshot
General Size-Change Termination and Lexicographic Descent
inferredcites →https://doi.org/10.1007/3-540-44667-2_7openalex-snapshot
Constructing Automata from Temporal Logic Formulas: A Tutorial⋆
inferredcites →https://doi.org/10.1007/3-540-45319-9_7openalex-snapshot
Automatic Deductive Verification with Invisible Invariants
inferredcites →https://doi.org/10.1007/978-1-4612-4222-2openalex-snapshot
Temporal Verification of Reactive Systems
inferredcites →https://doi.org/10.1007/978-3-319-08867-9_53openalex-snapshot
Termination Analysis by Learning Terminating Programs
inferredcites →https://doi.org/10.1007/978-3-319-12904-4_6openalex-snapshot
Infinite-State Model Checking of LTLR Formulas Using Narrowing
inferredcites →https://doi.org/10.1007/978-3-319-21690-4_4openalex-snapshot
Fairness Modulo Theory: A New Approach to LTL Software Model Checking
inferredcites →https://doi.org/10.1007/978-3-319-21690-4_40openalex-snapshot
Property-Directed Inference of Universal Invariants or Proving Their Absence
inferredcites →https://doi.org/10.1007/978-3-319-21690-4_6openalex-snapshot
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms
inferredcites →https://doi.org/10.1007/978-3-319-41528-4_15openalex-snapshot
Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
inferredcites →https://doi.org/10.1007/978-3-319-41528-4_23openalex-snapshot
From Shape Analysis to Termination Analysis in Linear Time
inferredcites →https://doi.org/10.1007/978-3-319-41579-6_2openalex-snapshot
What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
inferredcites →https://doi.org/10.1007/978-3-540-24622-0_20openalex-snapshot
A Complete Method for the Synthesis of Linear Ranking Functions
inferredcites →https://doi.org/10.1007/978-3-540-31980-1_9openalex-snapshot
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems
inferredcites →https://doi.org/10.1007/978-3-540-68679-8_22openalex-snapshot
The Temporal Logic of Rewriting: A Gentle Introduction
inferredcites →https://doi.org/10.1007/978-3-540-71070-7_24openalex-snapshot
iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
inferredcites →https://doi.org/10.1007/978-3-540-78800-3_24openalex-snapshot
Z3: An Efficient SMT Solver
inferredcites →https://doi.org/10.1007/978-3-642-14295-6_9openalex-snapshot
Termination Analysis with Compositional Transition Invariants
inferredcites →https://doi.org/10.1007/978-3-642-19835-9_2openalex-snapshot
Transition Invariants and Transition Predicate Abstraction for Program Termination
inferredcites →https://doi.org/10.1007/978-3-642-22110-1_11openalex-snapshot
State/Event-Based LTL Model Checking under Parametric Generalized Fairness
inferredcites →https://doi.org/10.1007/978-3-642-31424-7_12openalex-snapshot
Termination Analysis with Algorithmic Learning
inferredcites →https://doi.org/10.1007/978-3-642-54833-8_21openalex-snapshot
Automatic Termination Verification for Higher-Order Functional Programs
inferredcites →https://doi.org/10.1007/s10817-009-9161-6openalex-snapshot
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
inferredcites →https://doi.org/10.1016/0304-3975(89)90138-2openalex-snapshot
The power of temporal proofs
inferredcites →https://doi.org/10.1016/0304-3975(92)90182-fopenalex-snapshot
Conditional rewriting logic as a unified model of concurrency
inferredcites →https://doi.org/10.1016/j.cl.2015.10.001openalex-snapshot
Inference of ranking functions for proving temporal properties by abstract interpretation
inferredcites →https://doi.org/10.1016/j.entcs.2005.11.018openalex-snapshot
Liveness Checking as Safety Checking for Infinite State Spaces
inferredcites →https://doi.org/10.1016/j.jlap.2012.06.003openalex-snapshot
Twenty years of rewriting logic
inferredcites →https://doi.org/10.1016/j.scico.2014.02.006openalex-snapshot
Model checking linear temporal logic of rewriting formulas under localized fairness
inferredcites →https://doi.org/10.1016/s1571-0661(04)80410-9openalex-snapshot
Liveness Checking as Safety Checking
inferredcites →https://doi.org/10.1109/fmcad.2016.7886668openalex-snapshot
Modular specification and verification of a cache-coherent interface
inferredcites →https://doi.org/10.1109/time.2008.15openalex-snapshot
Practical First-Order Temporal Reasoning
inferredcites →https://doi.org/10.1112/plms/s2-30.1.264openalex-snapshot
On a Problem of Formal Logic
inferredcites →https://doi.org/10.1145/1133255.1134029openalex-snapshot
Termination proofs for systems code
inferredcites →https://doi.org/10.1145/1133981.1134029openalex-snapshot
Termination proofs for systems code
inferredcites →https://doi.org/10.1145/1190215.1190257openalex-snapshot
Proving that programs eventually do something good
inferredcites →https://doi.org/10.1145/1190216.1190257openalex-snapshot
Proving that programs eventually do something good
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/1753171.1753191openalex-snapshot
Reconfiguring a state machine
inferredcites →https://doi.org/10.1145/2103621.2103687openalex-snapshot
An abstract interpretation framework for termination
inferredcites →https://doi.org/10.1145/2103656.2103687openalex-snapshot
An abstract interpretation framework for termination
inferredcites →https://doi.org/10.1145/2737924.2737958openalex-snapshot
Verdi: a framework for implementing and formally verifying distributed systems
inferredcites →https://doi.org/10.1145/2837614.2837650openalex-snapshot
PSync: a partially synchronous language for fault-tolerant distributed algorithms
inferredcites →https://doi.org/10.1145/2837614.2837667openalex-snapshot
Temporal verification of higher-order functional programs
inferredcites →https://doi.org/10.1145/2908080.2908118openalex-snapshot
Ivy: safety verification by interactive generalization
inferredcites →https://doi.org/10.1145/2914770.2837650openalex-snapshot
PSync: a partially synchronous language for fault-tolerant distributed algorithms
inferredcites →https://doi.org/10.1145/2933575.2935310openalex-snapshot
Proving Liveness of Parameterized Programs
inferredcites →https://doi.org/10.1145/3009837.3009860openalex-snapshot
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
inferredcites →https://doi.org/10.1145/3009837.3009893openalex-snapshot
Thread modularity at many levels: a pearl in compositional verification
inferredcites →https://doi.org/10.1145/3140568openalex-snapshot
Paxos made EPR: decidable reasoning about distributed protocols
inferredcites →https://doi.org/10.1145/3149.214121openalex-snapshot
Impossibility of distributed consensus with one faulty process
inferredcites →https://doi.org/10.1145/360204.360210openalex-snapshot
The size-change principle for program termination
inferredcites →https://doi.org/10.1145/361082.361093openalex-snapshot
A new solution of Dijkstra's concurrent programming problem
inferredcites →https://doi.org/10.1145/514188.514190openalex-snapshot
Parametric shape analysis via 3-valued logic
inferredcites →https://doi.org/10.1145/68182.68193openalex-snapshot
Translation lookaside buffer consistency: a software approach
inferredcites →https://doi.org/10.1145/70082.68193openalex-snapshot
Translation lookaside buffer consistency: a software approach
inferredcites →https://doi.org/10.2200/s00658ed1v01y201508dct013openalex-snapshot
Decidability of Parameterized Verification
inferredcites →https://doi.org/10.5555/3077629.3077651openalex-snapshot
Modular specification and verification of a cache-coherent interface
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.2139/ssrn.4623116openalex-extracted
Prenex Universal First-Order Safety Properties
inferred← citeshttps://doi.org/10.1007/978-3-030-30942-8_5openalex-snapshot
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
inferred← citeshttps://doi.org/10.1007/978-3-030-53291-8_12openalex-snapshot
Ivy: A Multi-modal Verification Tool for Distributed Algorithms
inferred← citeshttps://doi.org/10.1007/978-3-030-81688-9_16openalex-snapshot
Sound Verification Procedures for Temporal Properties of Infinite-State Systems
inferred← citeshttps://doi.org/10.1007/978-3-030-99524-9_18openalex-snapshot
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
inferred← citeshttps://doi.org/10.1007/978-3-031-65627-9_13openalex-snapshot
Toward Liveness Proofs at Scale
inferred← citeshttps://doi.org/10.1007/978-3-031-86695-1_2openalex-snapshot
Towards Verifying Security Policies for Infinite-State Systems
inferred← citeshttps://doi.org/10.1007/978-3-031-90643-5_20openalex-snapshot
Implicit Rankings for Verifying Liveness Properties in First-Order Logic
inferred← citeshttps://doi.org/10.1007/978-3-032-13711-1_2openalex-snapshot
Liveness to Safety for Distributed Systems
inferred← citeshttps://doi.org/10.1007/978-3-032-22749-2_18openalex-snapshot
Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
inferred← citeshttps://doi.org/10.1007/978-3-032-32519-8_8openalex-snapshot
The TLA+ Model Checker Apalache
inferred← citeshttps://doi.org/10.1007/978-3-032-32537-2_1openalex-snapshot
Liveness Proofs for Hardware Model Checking
inferred← citeshttps://doi.org/10.1007/978-3-319-99725-4_4openalex-snapshot
Deductive Verification in Decidable Fragments with Ivy
inferred← citeshttps://doi.org/10.1007/s10703-021-00377-1openalex-snapshot
Temporal prophecy for proving temporal properties of infinite-state systems
inferred← citeshttps://doi.org/10.1007/s10703-023-00439-6openalex-snapshot
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
inferred← citeshttps://doi.org/10.1016/j.ic.2020.104641openalex-snapshot
A decidable and expressive fragment of Many-Sorted First-Order Linear Temporal Logic
inferred← citeshttps://doi.org/10.1016/j.ipl.2024.106488openalex-snapshot
Prenex universal first-order safety properties
inferred← citeshttps://doi.org/10.1109/sp63933.2026.00009openalex-snapshot
Mechanized Safety and Liveness Proofs for the Mysticeti Consensus Protocol Under the LiDO-DAG Framework
inferred← citeshttps://doi.org/10.1109/wacv48630.2021.00202openalex-snapshot
Interpretable and Trustworthy Deepfake Detection via Dynamic Prototypes
inferred← citeshttps://doi.org/10.1145/3276534openalex-snapshot
Safe replication through bounded concurrency verification
inferred← citeshttps://doi.org/10.1145/3296979.3192405openalex-snapshot
Advanced automata-based algorithms for program termination checking
inferred← citeshttps://doi.org/10.1145/3341301.3359636openalex-snapshot
Fast and secure global payments with Stellar
inferred← citeshttps://doi.org/10.1145/3354166.3354180openalex-snapshot
Moderately Complex Paxos Made Simple
inferred← citeshttps://doi.org/10.1145/3360564openalex-snapshot
Asphalion: trustworthy shielding against Byzantine faults
inferred← citeshttps://doi.org/10.1145/3385412.3386018openalex-snapshot
First-order quantified separators
inferred← citeshttps://doi.org/10.1145/3434325openalex-snapshot
Context-bounded verification of liveness properties for multithreaded shared-memory programs
inferred← citeshttps://doi.org/10.1145/3485534openalex-snapshot
QuickSilver: modeling and parameterized verification for distributed agreement-based systems
inferred← citeshttps://doi.org/10.1145/3632864openalex-snapshot
Regular Abstractions for Array Systems
inferred← citeshttps://doi.org/10.1145/3632877openalex-snapshot
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
inferred← citeshttps://doi.org/10.1145/3649826openalex-snapshot
AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects
inferred← citeshttps://doi.org/10.1145/3656423openalex-snapshot
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
inferred← citeshttps://doi.org/10.1145/3658644.3690355openalex-snapshot
Compositional Verification of Composite Byzantine Protocols
inferred← citeshttps://doi.org/10.1145/3729306openalex-snapshot
LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols
inferred← citeshttps://doi.org/10.1145/3830418.3843868openalex-snapshot
Welder: Compositional Liveness Verification of Cluster Control Planes
inferred← citeshttps://doi.org/10.23919/fmcad.2018.8603001openalex-snapshot
Analyzing the Fundamental Liveness Property of the Chord Protocol
inferred← citeshttps://doi.org/10.23919/fmcad.2018.8603008openalex-snapshot
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
inferred← citeshttps://doi.org/10.23919/fmcad.2018.8603010openalex-snapshot
Deductive Verification of Distributed Protocols in First-Order Logic
inferred← citeshttps://doi.org/10.23919/ifipnetworking70592.2026.11579070openalex-snapshot
JADE: Just A Deterministic Emulator to Support the Verification of Protocol Implementations
inferred← citeshttps://doi.org/10.3390/math9040368openalex-snapshot
A Divide and Conquer Approach to Eventual Model Checking
inferred← citeshttps://doi.org/10.46298/lmcs-19(1:17)2023openalex-snapshot
A case study on parametric verification of failure detectors
inferred← citeshttps://doi.org/10.48550/arxiv.1704.00082openalex-snapshot
Moderately Complex Paxos Made Simple: High-Level Executable Specification of Distributed Algorithms
inferred← citeshttps://doi.org/10.48550/arxiv.2001.04787openalex-snapshot
What's Live? Understanding Distributed Consensus
inferred← citeshttps://doi.org/10.48550/arxiv.2004.04613openalex-snapshot
QuickSilver: A Modeling and Parameterized Verification Framework for Systems with Distributed Agreement (Extended Version)
inferred← citeshttps://doi.org/10.70675/6a415ed3z09a7z4be9zb69ez54453f1311a0openalex-snapshot
Propriété du domaine borné pour la logique temporelle linéaire du premier ordre et applications à la vérification de systèmes à états infinis
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.