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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

DASA: Fully Gradient-Based Program Analysis (Competition Contribution)

  • Felix Mächtle,
  • Jan-Niclas Serr,
  • Nils Loose,
  • Thomas Eisenbarth

摘要

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.