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...
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | JOUR |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_16191366_v14_n1_p45_CuervoParrino |
| Aporte de: |
| id |
todo:paper_16191366_v14_n1_p45_CuervoParrino |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_16191366_v14_n1_p45_CuervoParrino2023-10-03T16:28:31Z TacoFlow: optimizing SAT program verification using dataflow analysis Cuervo Parrino, B. Galeotti, J.P. Garbervetsky, D. Frias, M.F. 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. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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 Cuervo Parrino, B. Galeotti, J.P. Garbervetsky, D. Frias, M.F. 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. |
| format |
JOUR |
| author |
Cuervo Parrino, B. Galeotti, J.P. Garbervetsky, D. Frias, M.F. |
| author_facet |
Cuervo Parrino, B. Galeotti, J.P. Garbervetsky, D. Frias, M.F. |
| author_sort |
Cuervo Parrino, B. |
| 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 |
| url |
http://hdl.handle.net/20.500.12110/paper_16191366_v14_n1_p45_CuervoParrino |
| work_keys_str_mv |
AT cuervoparrinob tacoflowoptimizingsatprogramverificationusingdataflowanalysis AT galeottijp tacoflowoptimizingsatprogramverificationusingdataflowanalysis AT garbervetskyd tacoflowoptimizingsatprogramverificationusingdataflowanalysis AT friasmf tacoflowoptimizingsatprogramverificationusingdataflowanalysis |
| _version_ |
1782026664240218112 |