Cover Image

Hyperproperty Verification as CHC Satisfiability

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Itzhaky, Shachar, Shoham, Sharon, Vizel, Yakir
Format:	Preprint
Published:	2023
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Revisiting DRUP-based Interpolants with CaDiCaL 2.0
by: Khouri, Basel, et al.
Published: (2025)

Property Directed Reachability with Extended Resolution
by: Luka, Andrew, et al.
Published: (2025)

Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
by: Peled, Romy, et al.
Published: (2025)

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

Visualizing Game-Based Certificates for Hyperproperty Verification
by: Beutner, Raven, et al.
Published: (2025)

On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
by: Beutner, Raven, et al.
Published: (2025)

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

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

CHC-COMP 2023: Competition Report
by: De Angelis, Emanuele, et al.
Published: (2024)

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

Explainability Requirements as Hyperproperties
by: Finkbeiner, Bernd, et al.
Published: (2025)

Logics and Algorithms for Hyperproperties
by: Finkbeiner, Bernd
Published: (2025)

Tractable Hyperproperties for MDPs
by: Gerlach, Lina, et al.
Published: (2026)

Temporal Hyperproperties for Population Protocols
by: Waldburger, Nicolas, et al.
Published: (2024)

Unifying Asynchronous Logics for Hyperproperties
by: Bombardelli, Alberto, et al.
Published: (2024)

Reasoning about Quality in Hyperproperties
by: Graepler, Samuel, et al.
Published: (2025)

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

Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving
by: Bembenek, Aaron, et al.
Published: (2026)

Non-Deterministic Planning for Hyperproperty Verification
by: Beutner, Raven, et al.
Published: (2024)

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

Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
by: Sebastiani, Roberto
Published: (2025)

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)

HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
by: Beutner, Raven, et al.
Published: (2022)

Decentralized Planning Using Probabilistic Hyperproperties
by: Pontiggia, Francesco, et al.
Published: (2025)

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
by: Dardinier, Thibault, et al.
Published: (2023)

TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets
by: Gonzalez, Bruno Maria René, et al.
Published: (2025)

Syntax-Guided Automated Program Repair for Hyperproperties
by: Beutner, Raven, et al.
Published: (2024)

Centralized vs Decentralized Monitors for Hyperproperties
by: Aceto, Luca, et al.
Published: (2024)

Satisfiability of Quantified Boolean Announcements
by: van Ditmarsch, Hans, et al.
Published: (2022)

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

Logics for Context-free Hyperproperties
by: Winter, Sarah, et al.
Published: (2026)

HypRL: Reinforcement Learning of Control Policies for Hyperproperties
by: Hsu, Tzu-Han, et al.
Published: (2025)

On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties
by: Beutner, Raven, et al.
Published: (2025)

HyperQB: A Bounded Model Checker for Hyperproperties
by: Hsu, Tzu-Han, et al.
Published: (2021)

Satisfiability Modulo Exponential Integer Arithmetic
by: Frohn, Florian, et al.
Published: (2024)

Finding Connections via Satisfiability Solving
by: Eisenhofer, Clemens, et al.
Published: (2026)

Spanning Matrices via Satisfiability Solving
by: Eisenhofer, Clemens, et al.
Published: (2024)

Strategy Logic, Imperfect Information, and Hyperproperties
by: Beutner, Raven, et al.
Published: (2025)

Satisfiability in Łukasiewicz logic and its unbounded relative
by: Haniková, Zuzana, et al.
Published: (2025)

Satisfiability Modulo Theories for Verifying MILP Certificates
by: Wood, Kenan, et al.
Published: (2023)