Automatic Detection of Vulnerable Variables for CTL Properties of Programs

We present our tool FuncTion-V for the automatic identification of the minimal sets of program variables that an attacker can control to ensure an undesirable program property. FuncTion-V supports program properties expressed in Computation Tree Logic (CTL), and builds upon an abstract interpretation-based static analysis for CTL properties that we extend with an abstraction refinement process. We showcase our tool on benchmarks collected from the literature and SV-COMP 2023.