TacoFlow: optimizing SAT program verification using dataflow analysis

CUERVO PARRINO , BRUNO; GALEOTTI, JUAN PABLO; GARBERVETSKY, DIEGO; FRIAS, MARCELO FABIAN

SOFTWARE AND SYSTEMS MODELING

SPRINGER HEIDELBERG

Lugar: HEIDELBERG; Año: 2015 vol. 14 p. 45 - 63

1619-1366

InpreviousworkwepresentedTACO,atoolforefficientbounded verification. TACO translates programs annotated with contracts to a SAT problem which is then solved resorting to off-the-shelf SAT-solvers. TACO may deem propositional variables used in the description of a program ini- tial states as being unnecessary. Since the worst-case complexity of SAT (a known NP problem) depends on the number of variables, most times this al- lows us to obtain significant speed ups. In this article we present TacoFlow, an improvement over TACO that uses dataflow analysis in order to also discard propositional variables that describe intermediate program states. We present an extensive empirical evaluation that considers the effect of removing those variables at different levels of abstraction, and a discussion on the benefits of the proposed approach.