A dataflow analysis to improve SAT-based bounded program verification
SAT-based bounded verification of programs consists of the translation of the code and its annotations into a propositional formula. The formula is then analyzed for specification violations using a SAT-solver. This technique is capable of proving the absence of errors up to a given scope. SAT is a...
Guardado en:
Autores principales: | , , , |
---|---|
Formato: | SER |
Materias: | |
Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_03029743_v7041LNCS_n_p138_CuervoParrino |
Aporte de: |
id |
todo:paper_03029743_v7041LNCS_n_p138_CuervoParrino |
---|---|
record_format |
dspace |
spelling |
todo:paper_03029743_v7041LNCS_n_p138_CuervoParrino2023-10-03T15:19:22Z A dataflow analysis to improve SAT-based bounded program verification Cuervo Parrino, B. Galeotti, J.P. Garbervetsky, D. Frias, M.F. Bounded program verifications Empirical evaluations Logical representations NP complete problems Propositional formulas Propositional variables SAT solvers SAT-based bounded verification Verification tools Computational complexity Data flow analysis Formal logic Program translators Verification Formal methods SAT-based bounded verification of programs consists of the translation of the code and its annotations into a propositional formula. The formula is then analyzed for specification violations using a SAT-solver. This technique is capable of proving the absence of errors up to a given scope. SAT is a well-known NP-complete problem, whose complexity depends on the number of propositional variables occurring in the formula. Thus, reducing the number of variables in the logical representation may have a great impact on the overall analysis. We propose a dataflow analysis which infers the set of possible values that can be assigned to each local and instance variable. Unnecessary variables at the SAT level can then be safely removed by relying on the inferred values. We implemented this approach in TACO, a SAT-based verification tool. We present an extensive empirical evaluation and discuss the benefits of the proposed approach. © 2011 Springer-Verlag. 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. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v7041LNCS_n_p138_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 |
Bounded program verifications Empirical evaluations Logical representations NP complete problems Propositional formulas Propositional variables SAT solvers SAT-based bounded verification Verification tools Computational complexity Data flow analysis Formal logic Program translators Verification Formal methods |
spellingShingle |
Bounded program verifications Empirical evaluations Logical representations NP complete problems Propositional formulas Propositional variables SAT solvers SAT-based bounded verification Verification tools Computational complexity Data flow analysis Formal logic Program translators Verification Formal methods Cuervo Parrino, B. Galeotti, J.P. Garbervetsky, D. Frias, M.F. A dataflow analysis to improve SAT-based bounded program verification |
topic_facet |
Bounded program verifications Empirical evaluations Logical representations NP complete problems Propositional formulas Propositional variables SAT solvers SAT-based bounded verification Verification tools Computational complexity Data flow analysis Formal logic Program translators Verification Formal methods |
description |
SAT-based bounded verification of programs consists of the translation of the code and its annotations into a propositional formula. The formula is then analyzed for specification violations using a SAT-solver. This technique is capable of proving the absence of errors up to a given scope. SAT is a well-known NP-complete problem, whose complexity depends on the number of propositional variables occurring in the formula. Thus, reducing the number of variables in the logical representation may have a great impact on the overall analysis. We propose a dataflow analysis which infers the set of possible values that can be assigned to each local and instance variable. Unnecessary variables at the SAT level can then be safely removed by relying on the inferred values. We implemented this approach in TACO, a SAT-based verification tool. We present an extensive empirical evaluation and discuss the benefits of the proposed approach. © 2011 Springer-Verlag. |
format |
SER |
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 |
A dataflow analysis to improve SAT-based bounded program verification |
title_short |
A dataflow analysis to improve SAT-based bounded program verification |
title_full |
A dataflow analysis to improve SAT-based bounded program verification |
title_fullStr |
A dataflow analysis to improve SAT-based bounded program verification |
title_full_unstemmed |
A dataflow analysis to improve SAT-based bounded program verification |
title_sort |
dataflow analysis to improve sat-based bounded program verification |
url |
http://hdl.handle.net/20.500.12110/paper_03029743_v7041LNCS_n_p138_CuervoParrino |
work_keys_str_mv |
AT cuervoparrinob adataflowanalysistoimprovesatbasedboundedprogramverification AT galeottijp adataflowanalysistoimprovesatbasedboundedprogramverification AT garbervetskyd adataflowanalysistoimprovesatbasedboundedprogramverification AT friasmf adataflowanalysistoimprovesatbasedboundedprogramverification AT cuervoparrinob dataflowanalysistoimprovesatbasedboundedprogramverification AT galeottijp dataflowanalysistoimprovesatbasedboundedprogramverification AT garbervetskyd dataflowanalysistoimprovesatbasedboundedprogramverification AT friasmf dataflowanalysistoimprovesatbasedboundedprogramverification |
_version_ |
1782024688083402752 |