Cover Image

CTL* Verification and Synthesis using Existential Horn Clauses

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Carelli, Mishel, Grumberg, Orna
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

Loop Termination and Generalized Collatz Sequences
by: Carelli, Mishel
Published: (2026)

Closure and Complexity of Temporal Causality
by: Carelli, Mishel, et al.
Published: (2025)

Proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis
by: De Angelis, Emanuele, et al.
Published: (2025)

Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
by: Katsura, Hiroyuki, et al.
Published: (2025)

Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
by: Somorjai, Márk, et al.
Published: (2024)

Catamorphic Abstractions for Constrained Horn Clause Satisfiability
by: De Angelis, Emanuele, et al.
Published: (2024)

HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
by: Jiang, Hongjian, et al.
Published: (2025)

Synthesis with Guided Environments
by: Kupferman, Orna, et al.
Published: (2025)

Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
by: Kutsia, Temur, et al.
Published: (2024)

Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures
by: Demri, Stephane, et al.
Published: (2023)

CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
by: Dobos-Kovács, Mihály, et al.
Published: (2025)

Synthesis with Privacy Against an Observer
by: Kupferman, Orna, et al.
Published: (2024)

Paraconsistent Existential Graphs Gamma Peirce System
by: Sierra-Aristizabal, Manuel
Published: (2023)

Towards Probabilistic Strategic Timed CTL
by: Jamroga, Wojciech, et al.
Published: (2026)

PICID: Proof-Driven Clause Learning in Neural Network Verification
by: Isac, Omri, et al.
Published: (2025)

Learning Branching-Time Properties in CTL and ATL via Constraint Solving
by: Bordais, Benjamin, et al.
Published: (2024)

HyperLTL Satisfiability Is Highly Undecidable, HyperCTL$^*$ is Even Harder
by: Fortin, Marie, et al.
Published: (2023)

Existential and positive games: a comonadic and axiomatic view
by: Abramsky, Samson, et al.
Published: (2025)

Universal Horn Sentences and the Joint Embedding Property
by: Bodirsky, Manuel, et al.
Published: (2021)

An abstract fixed-point theorem for Horn formula equations
by: Hetzl, Stefan, et al.
Published: (2025)

CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report)
by: Pettinau, Roberto, et al.
Published: (2026)

Partial Quantifier Elimination By Certificate Clauses
by: Goldberg, Eugene
Published: (2020)

Existential Positive Transductions of Sparse Graphs
by: Mählmann, Nikolas, et al.
Published: (2026)

Finite Axiomatizability by Disjunctive Existential Rules
by: Calautti, Marco, et al.
Published: (2025)

Rethinking Clause Management for CDCL SAT Solvers
by: Cai, Yalun, et al.
Published: (2026)

Equational Theorem Proving for Clauses over Strings
by: Kim, Dohan
Published: (2023)

Disjoint Partial Enumeration without Blocking Clauses
by: Spallitta, Giuseppe, et al.
Published: (2023)

Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
by: Lyon, Tim S., et al.
Published: (2026)

Open Horn Type Theory
by: Poernomo, Iman
Published: (2025)

Testing for Renamability to Classes of Clause Sets
by: Brandl, Albert, et al.
Published: (2025)

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
by: Spallitta, Giuseppe, et al.
Published: (2024)

Extended Resolution Clause Learning via Dual Implication Points
by: Buss, Sam, et al.
Published: (2024)

The Existential Theory of the Reals with Summation Operators
by: Bläser, Markus, et al.
Published: (2024)

Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations
by: Nakamura, Yoshiki
Published: (2023)

Existential Notation3 Logic
by: Arndt, Dörthe, et al.
Published: (2023)

On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number
by: Gallego-Hernández, Jorge, et al.
Published: (2025)

Efficient Neural Clause-Selection Reinforcement
by: Suda, Martin
Published: (2025)

Identifying Tractable Quantified Temporal Constraints within Ord-Horn
by: Rydval, Jakub, et al.
Published: (2024)

Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms (Full Version)
by: Takahata, Kanta, et al.
Published: (2025)

Theta as a Horn Solver
by: Bajczi, Levente, et al.
Published: (2025)