Cover Image

Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Lotan, Raz, Elad, Neta, Padon, Oded, Shoham, Sharon
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Programming Languages F.3.1; I.2.2
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Implicit Rankings for Verifying Liveness Properties in First-Order Logic
by: Lotan, Raz, et al.
Published: (2024)

Proving Cutoff Bounds for Safety Properties in First-Order Logic
by: Lotan, Raz, et al.
Published: (2024)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
by: Elad, Neta, et al.
Published: (2023)

Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
by: Yang, Ziyi, et al.
Published: (2026)

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
by: Frenkel, Eden, et al.
Published: (2026)

Translating Three-Variable First-Order Predicate Logic to Relation Algebra, Implemented using Z3
by: Brogni, Anthony, et al.
Published: (2023)

Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property
by: Elad, Neta, et al.
Published: (2026)

From Scientific Texts to Verifiable Code: Automating the Process with Transformers
by: Wang, Changjie, et al.
Published: (2025)

A Quadratic Lower Bound for Simulation
by: Groote, Jan Friso, et al.
Published: (2024)

Extremal Separation Problems for Temporal Instance Queries
by: Jung, Jean Christoph, et al.
Published: (2024)

FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines
by: Zhang, Xindi, et al.
Published: (2025)

Verification of Unbounded Client-Server Systems with Distinguishable Clients
by: Phawade, Ramchandra, et al.
Published: (2026)

Unravelling Abstract Cyclic Proofs into Proofs by Induction
by: Grotenhuis, Lide, et al.
Published: (2026)

Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned
by: Villadsen, Jørgen
Published: (2025)

ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings
by: Jana, Prithwish, et al.
Published: (2025)

Data Verification is the Future of Quantum Computing Copilots
by: Song, Junhao, et al.
Published: (2026)

Non-Ground Congruence Closure
by: Leidinger, Hendrik, et al.
Published: (2024)

Taming Differentiable Logics with Coq Formalisation
by: Affeldt, Reynald, et al.
Published: (2024)

Converting BPMN Diagrams to Privacy Calculus
by: Pitsiladis, Georgios V., et al.
Published: (2024)

Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
by: Frenkel, Eden, et al.
Published: (2024)

Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams
by: Lin, Yi, et al.
Published: (2025)

Teaching Higher-Order Logic Using Isabelle
by: Lund, Simon Tobias, et al.
Published: (2024)

Formal Verification of COO to CSR Sparse Matrix Conversion (Invited Paper)
by: Appel, Andrew W.
Published: (2025)

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
by: Klaus, Natalia, et al.
Published: (2026)

From Pixels to Privacy: Temporally Consistent Video Anonymization via Token Pruning for Privacy Preserving Action Recognition
by: Aslam, Nazia, et al.
Published: (2026)

When do homomorphism counts help in query algorithms?
by: Cate, Balder ten, et al.
Published: (2023)

Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs
by: de Rezende, Susanna F., et al.
Published: (2019)

Infinitary Refinement Types for Temporal Properties in Scott Domains
by: Riba, Colin, et al.
Published: (2025)

Axe 'Em: Eliminating Spurious States with Induction Axioms
by: Elad, Neta, et al.
Published: (2024)

Dormancy-aware timed branching bisimilarity, with an application to communication protocol analysis
by: Middelburg, C. A.
Published: (2021)

Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol
by: Praveen, M., et al.
Published: (2024)

Formal Methods for Mobile Ad Hoc Networks: A Survey
by: Fokkink, Wan, et al.
Published: (2025)

Constant time testability of first-order logic with modulo counting on finitary graphs
by: Adler, Isolde, et al.
Published: (2026)

Verified VCG and Verified Compiler for Dafny
by: Nezamabadi, Daniel, et al.
Published: (2025)

Predictable Gradient Manifolds in Deep Learning: Temporal Path-Length and Intrinsic Rank as a Complexity Regime
by: Calvo, Anherutowa
Published: (2026)

Train to Defend: First Defense Against Cryptanalytic Neural Network Parameter Extraction Attacks
by: Kurian, Ashley, et al.
Published: (2025)

Constrained LTL Specification Learning from Examples
by: Zhang, Changjian, et al.
Published: (2024)

Bounded Model Checking for Unbounded Client Server Systems
by: Phawade, Ramchandra, et al.
Published: (2022)

Software Implementation of Digital Filtering via Tustin's Bilinear Transform
by: Herron, Connor W.
Published: (2024)

Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity
by: Knop, Dušan, et al.
Published: (2017)