Cover Image

Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Frenkel, Eden, Chajed, Tej, Padon, Oded, Shoham, Sharon
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
by: Lotan, Raz, et al.
Published: (2026)

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

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
by: Tsukada, Takeshi, et al.
Published: (2025)

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

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

Hyperproperty Verification as CHC Satisfiability
by: Itzhaky, Shachar, et al.
Published: (2023)

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

Identifying and Explaining (Non-)Equivalence of First-Order Logic Formulas
by: Vehlken, Fabian, et al.
Published: (2026)

Symmetries of Dependency Quantified Boolean Formulas
by: Hofstadler, Clemens, et al.
Published: (2024)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
by: Elad, Neta, et al.
Published: (2025)

Model Counting for Dependency Quantified Boolean Formulas
by: Fung, Long-Hin, et al.
Published: (2025)

Unravelling Cyclic First-Order Arithmetic
by: Leigh, Graham E., et al.
Published: (2025)

Minimally Comparing Relational Abstract Domains
by: Ballou, Kenny, et al.
Published: (2023)

Complexity of Weighted First-Order Model Counting in the Two-Variable Fragment with Counting Quantifiers: A Bound to Beat
by: Tóth, Jan, et al.
Published: (2024)

Identifying Minimal Changes in the Zone Abstract Domain
by: Ballou, Kenny, et al.
Published: (2023)

Efficient Volume Computation for SMT Formulas
by: Shaw, Arijit, et al.
Published: (2025)

A Game for Counting Logic Formula Size and an Application to Linear Orders
by: Fournier, Gregoire, et al.
Published: (2025)

Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms
by: de Lima, Thaynara Arielly, et al.
Published: (2024)

Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions
by: Artale, Alessandro, et al.
Published: (2025)

Distributed First Order Logic
by: Ghidini, Chiara, et al.
Published: (2015)

Interpolation in First-Order Logic
by: Cate, Balder ten, et al.
Published: (2025)

Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
by: Finkbeiner, Bernd, et al.
Published: (2026)

Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
by: Lyon, Tim S., et al.
Published: (2024)

Monitoring Second-Order Hyperproperties
by: Beutner, Raven, et al.
Published: (2024)

On Efficient Algorithms For Partial Quantifier Elimination
by: Goldberg, Eugene
Published: (2024)

Interpolation with Automated First-Order Reasoning
by: Wernhard, Christoph
Published: (2025)

Extended Abstract: Mutable Objects with Several Implementations
by: Kaufmann, Matt, et al.
Published: (2025)

SAT Solving for Variants of First-Order Subsumption
by: Coutelier, Robin, et al.
Published: (2024)

Craig Interpolation for Decidable First-Order Fragments
by: Cate, Balder ten, et al.
Published: (2023)

On the Satisfiability of Local First-Order Logics with Data
by: Bollig, Benedikt, et al.
Published: (2023)

First Order Logic with Fuzzy Semantics for Describing and Recognizing Nerves in Medical Images
by: Bloch, Isabelle, et al.
Published: (2025)

An Abstract Domain for Heap Commutativity (Extended Version)
by: Pincus, Jared, et al.
Published: (2024)

Embedded Finite Models Beyond Restricted Quantifier Collapse
by: Benedikt, Michael, et al.
Published: (2023)

Fusions of One-Variable First-Order Modal Logics
by: Kontchakov, Roman, et al.
Published: (2026)

On Knowledge Compilation For Two-Variable First-Order Logic
by: Meng, Qiaolan, et al.
Published: (2026)

Checking Satisfiability of Hyperproperties using First-Order Logic
by: Beutner, Raven, et al.
Published: (2025)

First-Order LTLf Synthesis with Lookback (Extended Version)
by: Winkler, Sarah
Published: (2025)

Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
by: Gheorghiu, Alexander V., et al.
Published: (2023)