.png){kind=icon}
.png){kind=icon}
Return
Modular invariant generation via constraint solving
.png){kind=icon}
PRE
AI
Z
Y
H
G
DOI：10.1016/j.sysarc.2026.103884.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Modular arithmetic is widely used in modern programs, including applications in cryptography, security checks, hash computations, and low-level system implementations. Existing analysis methods often focus on fixed moduli, limiting their applicability. In this work, we propose a general approach to eliminate the analysis barriers introduced by modular operations in loop programs, which extends Farkas’ Lemma-based invariant constraint solving techniques to programs with general modular operations. We define modular-related variables in the program and present a location-splitting technique to split the original program locations based on modular results and eliminate modular conditions from the transitions. This process results in an equivalent linear transition system free of modular information, which can be further used to generate invariants through constraint solving methods based on Farkas’ Lemma. We integrate this method into the existing StInG toolchain as a publicly available tool, Modular InvG, and evaluate it through a unified pipeline on manually constructed benchmarks and selected SV-COMP benchmarks, including comparisons with a strength-reduction baseline and CPAchecker. Experimental results demonstrate both the practical utility and high efficiency of our approach while preserving analysis precision. This work introduces a new direction for static analysis of programs with generalized modular arithmetic and lays the foundation for further optimization on large-scale benchmarks.
Journal
IF:
4.1
Papers:
2.9K
Citations:
4.2K
Organization
Cited Papers