.png){kind=icon}
.png){kind=icon}
Return
Hetrify+: Improving the Verification Efficiency of RISC-V Heterogeneous Programs via Memory Access Specialization
.png){kind=icon}
PRE
AI
Y
J
L
W
S
J
DOI：10.1109/tse.2026.3692469.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Heterogeneous software systems, which often combine closed-source libraries with exported interfaces, embedded assembly, and components in multiple languages, present significant challenges for formal verification. Our prior work, Hetrify, addressed this by converting RISC-V binaries into semantically equivalent C code, making such programs amenable to verification. However, its unified memory model required frequent dynamic computation of stack addresses, which significantly increased the size of the generated logical formulas, along with high memory usage and longer verification times. To address this, we propose memory access specialization, a static analysis and transformation technique that recovers fixed stack offsets during binary conversion to reduce verification overhead. By replacing symbolic stack accesses with fixed-offset memory references, it eliminates dynamic pointer arithmetic and reduces symbolic encoding complexity. This technique is integrated into Hetrify+, an enhanced verification tool for heterogeneous programs. To validate the effectiveness of our approach, we conduct both formal analysis and extensive empirical evaluation. Formal analysis guarantees the correctness of our method. In our evaluation, Hetrify+ demonstrates the same verification accuracy as the original Hetrify on 100 low-level RISC-V assembly programs, achieving up to 2.5<inline-formula><tex-math notation="LaTeX">$\boldsymbol{\times}$</tex-math></inline-formula> speedup and 4.9<inline-formula><tex-math notation="LaTeX">$\boldsymbol{\times}$</tex-math></inline-formula> reduction in memory usage. For 30 large-scale heterogeneous programs that include binary-only components, Hetrify+ maintains a 100% success rate, reducing verification time by 1.9<inline-formula><tex-math notation="LaTeX">$\boldsymbol{\times}$</tex-math></inline-formula> and memory consumption by 1.2<inline-formula><tex-math notation="LaTeX">$\boldsymbol{\times}$</tex-math></inline-formula>. These results demonstrate that memory access specialization is key to scaling the verification of heterogeneous programs.
Keywords:
Heterogeneous program
RISC-V
memory access specialization
program verification
Journal
IF:
5.6
Papers:
2.8K
Citations:
1.1W
Organization
Cited Papers