Cover Image

Formally Verified Binary-level Pointer Analysis

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Verbeek, Freek, Shokri, Ali, Engel, Daniel, Ravindran, Binoy
Format:	Preprint
Published:	2025
Subjects:	Software Engineering
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

ENCRUST: Encapsulated Substitution and Agentic Refinement on a Live Scaffold for Safe C-to-Rust Translation
by: Sim, Hohyun, et al.
Published: (2026)

Adding Compilation Metadata To Binaries To Make Disassembly Decidable
by: Engel, Daniel, et al.
Published: (2026)

Search-Based Multi-Trajectory Refinement for Safe C-to-Rust Translation with Large Language Models
by: Sim, HoHyun, et al.
Published: (2025)

The Effect of Pointer Analysis on Semantic Conflict Detection
by: Barbosa, Matheus, et al.
Published: (2025)

Context-Sensitive Pointer Analysis for ArkTS
by: Yang, Yizhuo, et al.
Published: (2026)

Boosting Pointer Analysis With LLM-Enhanced Allocation Function Detection
by: Cheng, Baijun, et al.
Published: (2025)

Enhancing Semantic Understanding in Pointer Analysis using Large Language Models
by: Cheng, Baijun, et al.
Published: (2025)

IPSynth: Interprocedural Program Synthesis for Software Security Implementation
by: Shokri, Ali, et al.
Published: (2024)

Seneca: Taint-Based Call Graph Construction for Java Object Deserialization
by: Santos, Joanna C. S., et al.
Published: (2023)

KBX: Verified Model Synchronization via Formal Bidirectional Transformation
by: Zhao, Jianhong, et al.
Published: (2024)

Augmented Weak Distance for Fast and Accurate Bounds Checking
by: Fu, Zhoulai, et al.
Published: (2025)

LogPTR: Variable-Aware Log Parsing with Pointer Network
by: Wu, Yifan, et al.
Published: (2024)

Identifying Root Causes of Null Pointer Exceptions with Logical Inferences
by: Kim, Jindae, et al.
Published: (2024)

FormalRTL: Verified RTL Synthesis at Scale
by: Li, Kezhi, et al.
Published: (2026)

Enhanced LLM-Based Framework for Predicting Null Pointer Dereference in Source Code
by: Sultan, Md. Fahim, et al.
Published: (2024)

Formally and Empirically Verified Methodologies for Scalable Hierarchical Full-Stack Systems
by: Liu, Dong
Published: (2025)

VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models
by: Sevenhuijsen, Merlijn, et al.
Published: (2024)

Flow Sensitivity without Control Flow Graph: An Efficient Andersen-Style Flow-Sensitive Pointer Analysis
by: Zhang, Jiahao, et al.
Published: (2025)

BinaryAI: Binary Software Composition Analysis via Intelligent Binary Source Code Matching
by: Jiang, Ling, et al.
Published: (2024)

VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications
by: Misu, Md Rakib Hossain, et al.
Published: (2026)

Project-Level C-to-Rust Translation via Pointer Knowledge Graphs
by: Yuan, Zhiqiang, et al.
Published: (2025)

ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks
by: Wei, Tianhao, et al.
Published: (2024)

Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
by: Bucev, Mario, et al.
Published: (2024)

Formal Analysis of Reachability, Infection and Propagation Conditions in Mutation Testing
by: Mirian-Hosseinabadi, Seyed-Hassan
Published: (2024)

Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study
by: Menezes, Rafael Sá, et al.
Published: (2024)

ExecVerify: White-Box RL with Verifiable Stepwise Rewards for Code Execution Reasoning
by: Tang, Lingxiao, et al.
Published: (2026)

Formal Analysis of Metastable Failures in Software Systems
by: Alvaro, Peter, et al.
Published: (2025)

The Opaque Pointer Design Pattern in Python: Towards a Pythonic PIMPL for Modularity, Encapsulation, and Stability
by: Saravanos, Antonios, et al.
Published: (2026)

Crash-free Deductive Verifiers
by: Nauta, Wander, et al.
Published: (2026)

Verify Linearizability of Concurrent Stacks
by: Wen, Tangliu
Published: (2021)

Raw Pointer Rewriting with LLMs for Translating C to Safer Rust
by: Gao, Yifei, et al.
Published: (2025)

From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification
by: Erfan, Md, et al.
Published: (2026)

Verify Implementation Equivalence of Large Models
by: Zhan, Qi, et al.
Published: (2026)

HALF: Hollowing Analysis Framework for Binary Programs with Kernel Module Assistance
by: Long, Zhangbo, et al.
Published: (2025)

Neurosymbolic Architectural Reasoning: Towards Formal Analysis through Neural Software Architecture Inference
by: Herbold, Steffen, et al.
Published: (2025)

Vital: Vulnerability-Oriented Symbolic Execution via Type-Unsafe Pointer-Guided Monte Carlo Tree Search
by: Tu, Haoxin, et al.
Published: (2024)

Formally Verifying Noir Zero Knowledge Programs with NAVe
by: Antonino, Pedro, et al.
Published: (2026)

BinMetric: A Comprehensive Binary Analysis Benchmark for Large Language Models
by: Shang, Xiuwei, et al.
Published: (2025)

Formalisms for Robotic Mission Specification and Execution: A Comparative Analysis
by: Filippone, Gianluca, et al.
Published: (2026)

Verifier Warnings Do Not Improve Comprehensibility Prediction
by: De Silva, Nadeeshan, et al.
Published: (2026)