Cover Image

Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Bembenek, Aaron, Murray, Toby
Format:	Preprint
Published:	2026
Subjects:	Programming Languages Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Equational Bit-Vector Solving via Strong Gröbner Bases
by: Song, Jiaxin, et al.
Published: (2024)

Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning
by: Luo, Ziyan, et al.
Published: (2023)

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

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

DateSAT: A Framework for Solving Date and Period Constraints
by: Cui, Leyi, et al.
Published: (2026)

Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
by: Cristiá, Maximiliano, et al.
Published: (2022)

Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
by: Lindner, Andreas, et al.
Published: (2023)

Denotational Foundations for Expected Cost Analysis
by: de Amorim, Pedro H. Azevedo
Published: (2024)

Structural Analysis of GRAFCET Control Specifications
by: Schnakenbeck, Aron, et al.
Published: (2023)

Termination Analysis of Linear-Constraint Programs
by: Ben-Amram, Amir M., et al.
Published: (2025)

Polymorphic Metaprogramming with Memory Management -- An Adjoint Analysis of Metaprogramming
by: Jang, Junyoung, et al.
Published: (2024)

Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement
by: Govindankutty, Arun
Published: (2026)

Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
by: Lee, Jaeseo, et al.
Published: (2025)

A Type System for Data Flow and Alias Analysis in ReScript
by: Lund, Nicky Ask, et al.
Published: (2024)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
by: Castagna, Giuseppe, et al.
Published: (2024)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
by: Rustenholz, Louis, et al.
Published: (2024)

FO-Complete Program Verification for Heap Logics
by: Murali, Adithya, et al.
Published: (2026)

A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct
by: Guha, Shibashis, et al.
Published: (2021)

Categorical Vector Space Semantics for Lambek Calculus with a Relevant Modality
by: McPheat, Lachlan, et al.
Published: (2020)

Customizing Static Analysis using Codesearch
by: Hayoun, Avi, et al.
Published: (2024)

Bean: A Language for Backward Error Analysis
by: Kellison, Ariel E., et al.
Published: (2025)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

Proceedings Sixth Workshop on Models for Formal Analysis of Real Systems
by: Lang, Frédéric, et al.
Published: (2024)

Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
by: Tao, Yichen, et al.
Published: (2026)

GNU Aris: a web application for students
by: Attri, Saksham, et al.
Published: (2025)

String Solving with Stabilization and Transducers (Technical Report)
by: Chocholatý, David, et al.
Published: (2026)

Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives
by: De Giacomo, Giuseppe, et al.
Published: (2025)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
by: Leutgeb, Lorenz, et al.
Published: (2022)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

CSLib: The Lean Computer Science Library
by: Barrett, Clark, et al.
Published: (2026)

Recursive Mutexes in Separation Logic
by: Du, Ke, et al.
Published: (2026)

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
by: Zhang, Cheng, et al.
Published: (2026)

Symmetric Proofs of Parameterized Programs
by: Cheng, Ruotong, et al.
Published: (2026)

Can LLMs Perform Synthesis?
by: Egolf, Derek, et al.
Published: (2026)

Type Theory With Erasure
by: Theocharis, Constantine, et al.
Published: (2026)

A Program Logic for Abstract (Hyper)Properties
by: Baldan, Paolo, et al.
Published: (2026)

Ordered Adjoint Logic (Extended Version)
by: Roshal, Sophia, et al.
Published: (2026)

TensorRocq: Enabling diagrammatic reasoning in Rocq
by: Caldwell, Benjamin, et al.
Published: (2026)