Analysis of invariants for efficient bounded verification

SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Code inv...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.
Formato: CONF
Materias:
Alloy
DynAlloy
KodKod
SAT-based code analysis
Static analysis
Automated techniques
Code analysis
Execution trace
Linked data structures
Orders of magnitude
Propositional formulas
Propositional variables
Prototype tools
SAT solvers
SAT-based bounded verification
SAT-solving
Sequential programs
Symmetry-breaking
Tight bound
Computer software selection and evaluation
Data structures
Java programming language
Software testing
Model checking
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_97816055_v_n_p25_Galeotti
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_97816055_v_n_p25_Galeotti
record_format dspace
spelling todo:paper_97816055_v_n_p25_Galeotti2023-10-03T16:44:07Z Analysis of invariants for efficient bounded verification Galeotti, J.P. Rosner, N. Pombo, C.G.L. Frias, M.F. Alloy DynAlloy KodKod SAT-based code analysis Static analysis Automated techniques Code analysis DynAlloy Execution trace KodKod Linked data structures Orders of magnitude Propositional formulas Propositional variables Prototype tools SAT solvers SAT-based bounded verification SAT-solving Sequential programs Symmetry-breaking Tight bound Computer software selection and evaluation Data structures Java programming language Software testing Static analysis Model checking SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this article we present TACO, a prototype tool which implements a novel, general and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument code analysis with a symmetry-breaking predicate that allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading in the experiments we have carried out to an improvement on the efficiency of the analysis of orders of magnitude, compared to the non-instrumented SAT-based analysis. We show that, in some cases, our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking or SMT-solving. © 2010 ACM. Fil:Galeotti, J.P. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Rosner, N. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Pombo, C.G.L. 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. CONF info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_97816055_v_n_p25_Galeotti
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Alloy
DynAlloy
KodKod
SAT-based code analysis
Static analysis
Automated techniques
Code analysis
DynAlloy
Execution trace
KodKod
Linked data structures
Orders of magnitude
Propositional formulas
Propositional variables
Prototype tools
SAT solvers
SAT-based bounded verification
SAT-solving
Sequential programs
Symmetry-breaking
Tight bound
Computer software selection and evaluation
Data structures
Java programming language
Software testing
Static analysis
Model checking
spellingShingle Alloy
DynAlloy
KodKod
SAT-based code analysis
Static analysis
Automated techniques
Code analysis
DynAlloy
Execution trace
KodKod
Linked data structures
Orders of magnitude
Propositional formulas
Propositional variables
Prototype tools
SAT solvers
SAT-based bounded verification
SAT-solving
Sequential programs
Symmetry-breaking
Tight bound
Computer software selection and evaluation
Data structures
Java programming language
Software testing
Static analysis
Model checking
Galeotti, J.P.
Rosner, N.
Pombo, C.G.L.
Frias, M.F.
Analysis of invariants for efficient bounded verification
topic_facet Alloy
DynAlloy
KodKod
SAT-based code analysis
Static analysis
Automated techniques
Code analysis
DynAlloy
Execution trace
KodKod
Linked data structures
Orders of magnitude
Propositional formulas
Propositional variables
Prototype tools
SAT solvers
SAT-based bounded verification
SAT-solving
Sequential programs
Symmetry-breaking
Tight bound
Computer software selection and evaluation
Data structures
Java programming language
Software testing
Static analysis
Model checking
description SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this article we present TACO, a prototype tool which implements a novel, general and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument code analysis with a symmetry-breaking predicate that allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading in the experiments we have carried out to an improvement on the efficiency of the analysis of orders of magnitude, compared to the non-instrumented SAT-based analysis. We show that, in some cases, our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking or SMT-solving. © 2010 ACM.
format CONF
author Galeotti, J.P.
Rosner, N.
Pombo, C.G.L.
Frias, M.F.
author_facet Galeotti, J.P.
Rosner, N.
Pombo, C.G.L.
Frias, M.F.
author_sort Galeotti, J.P.
title Analysis of invariants for efficient bounded verification
title_short Analysis of invariants for efficient bounded verification
title_full Analysis of invariants for efficient bounded verification
title_fullStr Analysis of invariants for efficient bounded verification
title_full_unstemmed Analysis of invariants for efficient bounded verification
title_sort analysis of invariants for efficient bounded verification
url http://hdl.handle.net/20.500.12110/paper_97816055_v_n_p25_Galeotti
work_keys_str_mv AT galeottijp analysisofinvariantsforefficientboundedverification
AT rosnern analysisofinvariantsforefficientboundedverification
AT pombocgl analysisofinvariantsforefficientboundedverification
AT friasmf analysisofinvariantsforefficientboundedverification
_version_ 1782028985684721664

Ejemplares similares