TacoFlow: optimizing SAT program verification using dataflow analysis

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...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Galeotti, Juan Pablo, Garbervetsky, Diego, Frias, Marcelo
Publicado:	2014
Materias:	Dataflow analysis Java-like programs verification SAT-based verification Boolean functions Computer software Formal logic Java programming language Bounded verifications Empirical evaluations Java-like programs Levels of abstraction Program Verification Propositional variables SAT-based Worst-case complexity Data flow analysis
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16191366_v14_n1_p45_CuervoParrino http://hdl.handle.net/20.500.12110/paper_16191366_v14_n1_p45_CuervoParrino
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_16191366_v14_n1_p45_CuervoParrino
record_format	dspace
spelling	paper:paper_16191366_v14_n1_p45_CuervoParrino2023-06-08T16:25:35Z TacoFlow: optimizing SAT program verification using dataflow analysis Galeotti, Juan Pablo Garbervetsky, Diego Frias, Marcelo Dataflow analysis Java-like programs verification SAT-based verification Boolean functions Computer software Formal logic Java programming language Bounded verifications Empirical evaluations Java-like programs Levels of abstraction Program Verification Propositional variables SAT-based Worst-case complexity Data flow analysis 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. © 2014, Springer-Verlag Berlin Heidelberg. Fil:Galeotti, J.P. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Garbervetsky, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Frias, M.F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2014 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16191366_v14_n1_p45_CuervoParrino http://hdl.handle.net/20.500.12110/paper_16191366_v14_n1_p45_CuervoParrino
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Dataflow analysis Java-like programs verification SAT-based verification Boolean functions Computer software Formal logic Java programming language Bounded verifications Empirical evaluations Java-like programs Levels of abstraction Program Verification Propositional variables SAT-based Worst-case complexity Data flow analysis
spellingShingle	Dataflow analysis Java-like programs verification SAT-based verification Boolean functions Computer software Formal logic Java programming language Bounded verifications Empirical evaluations Java-like programs Levels of abstraction Program Verification Propositional variables SAT-based Worst-case complexity Data flow analysis Galeotti, Juan Pablo Garbervetsky, Diego Frias, Marcelo TacoFlow: optimizing SAT program verification using dataflow analysis
topic_facet	Dataflow analysis Java-like programs verification SAT-based verification Boolean functions Computer software Formal logic Java programming language Bounded verifications Empirical evaluations Java-like programs Levels of abstraction Program Verification Propositional variables SAT-based Worst-case complexity Data flow analysis
description	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. © 2014, Springer-Verlag Berlin Heidelberg.
author	Galeotti, Juan Pablo Garbervetsky, Diego Frias, Marcelo
author_facet	Galeotti, Juan Pablo Garbervetsky, Diego Frias, Marcelo
author_sort	Galeotti, Juan Pablo
title	TacoFlow: optimizing SAT program verification using dataflow analysis
title_short	TacoFlow: optimizing SAT program verification using dataflow analysis
title_full	TacoFlow: optimizing SAT program verification using dataflow analysis
title_fullStr	TacoFlow: optimizing SAT program verification using dataflow analysis
title_full_unstemmed	TacoFlow: optimizing SAT program verification using dataflow analysis
title_sort	tacoflow: optimizing sat program verification using dataflow analysis
publishDate	2014
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16191366_v14_n1_p45_CuervoParrino http://hdl.handle.net/20.500.12110/paper_16191366_v14_n1_p45_CuervoParrino
work_keys_str_mv	AT galeottijuanpablo tacoflowoptimizingsatprogramverificationusingdataflowanalysis AT garbervetskydiego tacoflowoptimizingsatprogramverificationusingdataflowanalysis AT friasmarcelo tacoflowoptimizingsatprogramverificationusingdataflowanalysis
_version_	1768542100897398784

TacoFlow: optimizing SAT program verification using dataflow analysis

Ejemplares similares