Cover Image

Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Palmskog, Karl, Lindner, Andreas, Constable, Scott, Guanciale, Roberto, Nemati, Hamed
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic
by: Nemati, Hamed, et al.
Published: (2025)

Gradual C0: Symbolic Execution for Gradual Verification
by: DiVincenzo, Jenna, et al.
Published: (2022)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)
by: Lööw, Andreas, et al.
Published: (2024)

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
by: Foster, Simon, et al.
Published: (2024)

Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
by: Flinkow, Thomas, et al.
Published: (2026)

Runtime Verification of Interactions Using Automata
by: Weil-Kennedy, Chana, et al.
Published: (2025)

Model Checking as Program Verification by Abstract Interpretation (Extended Version)
by: Baldan, Paolo, et al.
Published: (2025)

Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics
by: Losavio, Lidia, et al.
Published: (2025)

Formal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis
by: Hadjiloizou, Loizos, et al.
Published: (2024)

Eidoku: A Neuro-Symbolic Verification Gate for LLM Reasoning via Structural Constraint Satisfaction
by: Miya, Shinobu
Published: (2025)

COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery
by: Blain, Dominik
Published: (2026)

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

Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures
by: Colvin, Robert J., et al.
Published: (2024)

Decidable By Construction: Design-Time Verification for Trustworthy AI
by: Haynes, Houston
Published: (2026)

Symbolic Computation for All the Fun
by: Brown, Chad E., et al.
Published: (2024)

Proofs as Execution Trees for the π-Calculus
by: Acclavio, Matteo, et al.
Published: (2024)

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

Craig Interpolation in Program Verification
by: Rümmer, Philipp
Published: (2026)

Tools at the Frontiers of Quantitative Verification
by: Andriushchenko, Roman, et al.
Published: (2024)

Verification of Configurable SRA Systems
by: Cimatti, Alessandro, et al.
Published: (2026)

Exhaustive Symbolic Integration: Integration by Differentiation and the Landscape of Symbolic Integrability
by: Desmond, Harry
Published: (2026)

On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions
by: Jensen, Nicolaj Ø., et al.
Published: (2025)

On Symbol Elimination and Uniform Interpolation in Theory Extensions
by: Sofronie-Stokkermans, Viorica
Published: (2025)

Efficient Synthesis of Symbolic Distributed Protocols by Sketching
by: Egolf, Derek, et al.
Published: (2024)

Formal Verification of Isothermal Chemical Reactors
by: Feyzishendi, Parivash, et al.
Published: (2025)

Runtime Verification for LTL in Stochastic Systems
by: Esparza, Javier, et al.
Published: (2025)

Neuro-Symbolic Verification of LLM Outputs for Data-Sensitive Domains (extended preprint)
by: Sigloch, Paul, et al.
Published: (2026)

User-Guided Verification of Security Protocols via Sound Animation
by: Ye, Kangfeng, et al.
Published: (2024)

Bounded Structural Model Finding with Symbolic Data Constraints
by: Boronat, Artur
Published: (2026)

A Hierarchy of Supermartingales for $ω$-Regular Verification
by: Kura, Satoshi, et al.
Published: (2025)

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

A Program Instrumentation Framework for Automatic Verification
by: Amilon, Jesper, et al.
Published: (2024)

Towards Term-based Verification of Diagrammatic Equivalence
by: Cailler, Julie, et al.
Published: (2026)

LOGSAFE: Logic-Guided Verification for Trustworthy Federated Time-Series Learning
by: Nguyen, Dung Thuy, et al.
Published: (2024)

Using Color Refinement to Boost Enumeration and Counting for Acyclic CQs of Binary Schemas
by: Riveros, Cristian, et al.
Published: (2024)

Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
by: Fang, Jian, et al.
Published: (2025)

Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
by: Hozzová, Petra, et al.
Published: (2025)

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols
by: Ratschan, Stefan, et al.
Published: (2026)

Omega-regular Verification and Control for Distributional Specifications in MDPs
by: Akshay, S., et al.
Published: (2025)