DASA: Fully Gradient-Based Program Analysis (Competition Contribution)
摘要
We present a novel approach to program analysis that models each instruction using a mathematically differentiable wrapper. This enables gradient-based optimization over program inputs to drive execution towards specific target states, such as assertion violations. Instead of enumerating execution paths or solving symbolic constraints, the program itself is transformed into a differentiable computation graph. By optimizing a loss function that represents the likelihood of reaching a target location, all execution paths are explored simultaneously within a single optimization process. This paper describes the design and implementation of DASA, a differentiable analysis framework for Java programs, and reports on its first participation in the Java category of SV-COMP 2026.