Artículo
TacoFlow: optimizing SAT program verification using dataflow analysis
Fecha de publicación:
01/2015
Editorial:
Springer Heidelberg
Revista:
Software and Systems Modeling
ISSN:
1619-1366
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
In previous work, we presented TACO, a tool for efficient bounded 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 initial states as being unnecessary. Since the worst-case complexity of SAT (a known NP problem) depends on the number of variables, most times this allows 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.
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(SEDE CENTRAL)
Articulos de SEDE CENTRAL
Articulos de SEDE CENTRAL
Citación
Cuervo Parrino, Bruno; Galeotti, Juan Pablo; Garbervetsky, Diego David; Frias, Marcelo Fabian; TacoFlow: optimizing SAT program verification using dataflow analysis; Springer Heidelberg; Software and Systems Modeling; 14; 1; 1-2015; 45-63
Compartir
Altmétricas