TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds

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 failure is exhibited. Code i...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Galeotti, J.P., Rosner, N., Lopez Pombo, C.G., Frias, M.F.
Formato: JOUR
Materias:
Alloy
DynAlloy
KodKod
SAT-based code analysis
Static analysis
Code analysis
Linked data structures
Propositional formulas
Propositional variables
SAT-based bounded verification
Sequential programs
Alloying
Cerium alloys
Computer software
Data handling
Data structures
Java programming language
Model checking
Program translators
Tools
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_00985589_v39_n9_p1283_Galeotti
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_00985589_v39_n9_p1283_Galeotti
record_format dspace
spelling todo:paper_00985589_v39_n9_p1283_Galeotti2023-10-03T14:56:59Z TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds Galeotti, J.P. Rosner, N. Lopez Pombo, C.G. Frias, M.F. Alloy DynAlloy KodKod SAT-based code analysis Static analysis Code analysis DynAlloy KodKod Linked data structures Propositional formulas Propositional variables SAT-based bounded verification Sequential programs Alloying Cerium alloys Computer software Data handling Data structures Java programming language Model checking Program translators Tools Static analysis 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 failure is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this paper, we present Translation of Annotated COde (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 which, on one hand, reduces the size of the search space by ignoring certain classes of isomorphic models and, on the other hand, 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 to an improvement of the efficiency of the analysis of orders of magnitude, compared to the noninstrumented 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. © 1976-2012 IEEE. 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:Lopez Pombo, C.G. 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_00985589_v39_n9_p1283_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
Code analysis
DynAlloy
KodKod
Linked data structures
Propositional formulas
Propositional variables
SAT-based bounded verification
Sequential programs
Alloying
Cerium alloys
Computer software
Data handling
Data structures
Java programming language
Model checking
Program translators
Tools
Static analysis
spellingShingle Alloy
DynAlloy
KodKod
SAT-based code analysis
Static analysis
Code analysis
DynAlloy
KodKod
Linked data structures
Propositional formulas
Propositional variables
SAT-based bounded verification
Sequential programs
Alloying
Cerium alloys
Computer software
Data handling
Data structures
Java programming language
Model checking
Program translators
Tools
Static analysis
Galeotti, J.P.
Rosner, N.
Lopez Pombo, C.G.
Frias, M.F.
TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds
topic_facet Alloy
DynAlloy
KodKod
SAT-based code analysis
Static analysis
Code analysis
DynAlloy
KodKod
Linked data structures
Propositional formulas
Propositional variables
SAT-based bounded verification
Sequential programs
Alloying
Cerium alloys
Computer software
Data handling
Data structures
Java programming language
Model checking
Program translators
Tools
Static analysis
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 failure is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this paper, we present Translation of Annotated COde (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 which, on one hand, reduces the size of the search space by ignoring certain classes of isomorphic models and, on the other hand, 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 to an improvement of the efficiency of the analysis of orders of magnitude, compared to the noninstrumented 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. © 1976-2012 IEEE.
format JOUR
author Galeotti, J.P.
Rosner, N.
Lopez Pombo, C.G.
Frias, M.F.
author_facet Galeotti, J.P.
Rosner, N.
Lopez Pombo, C.G.
Frias, M.F.
author_sort Galeotti, J.P.
title TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds
title_short TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds
title_full TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds
title_fullStr TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds
title_full_unstemmed TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds
title_sort taco: efficient sat-based bounded verification using symmetry breaking and tight bounds
url http://hdl.handle.net/20.500.12110/paper_00985589_v39_n9_p1283_Galeotti
work_keys_str_mv AT galeottijp tacoefficientsatbasedboundedverificationusingsymmetrybreakingandtightbounds
AT rosnern tacoefficientsatbasedboundedverificationusingsymmetrybreakingandtightbounds
AT lopezpombocg tacoefficientsatbasedboundedverificationusingsymmetrybreakingandtightbounds
AT friasmf tacoefficientsatbasedboundedverificationusingsymmetrybreakingandtightbounds
_version_ 1782025448734064640

Ejemplares similares