Analysis of invariants for efficient bounded verification

Mostrar todas las versiones(2)

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

Descripción completa

Detalles Bibliográficos
Autores principales: Galeotti, Juan Pablo, Rosner, Nicolás, López Pombo, Carlos G., Frías, Marcelo
Formato: Ponencias en Congresos publishedVersion
Lenguaje:Inglés
Publicado: 2022
Materias:
ANALISIS DE FALLAS
JAVA
ESTRUCTURA DE DATOS
Acceso en línea:http://ri.itba.edu.ar/handle/123456789/3891
Aporte de:
Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA) de Instituto Tecnológico de Buenos Aires (ITBA)
id I32-R138-123456789-3891
record_format dspace
spelling I32-R138-123456789-38912022-12-07T14:14:02Z Analysis of invariants for efficient bounded verification Galeotti, Juan Pablo Rosner, Nicolás López Pombo, Carlos G. Frías, Marcelo ANALISIS DE FALLAS JAVA ESTRUCTURA DE DATOS "SAT-based bounded veri cation of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for speci cation 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 elds. Experiments show that the translations to propositional formulas require signi cantly less propositional variables, leading in the experiments we have carried out to an improvement on the e ciency of the analysis of orders of magnitude, compared to the non instrumented SAT-based analysis. We show that, in somecases, our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking or SMT-solving." 2022-05-23T18:51:29Z 2022-05-23T18:51:29Z 2010-07 Ponencias en Congresos info:eu-repo/semantics/publishedVersion http://ri.itba.edu.ar/handle/123456789/3891 en info:eu-repo/semantics/altIdentifier/doi/10.1145/1831708.1831712 application/pdf
institution Instituto Tecnológico de Buenos Aires (ITBA)
institution_str I-32
repository_str R-138
collection Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA)
language Inglés
topic ANALISIS DE FALLAS
JAVA
ESTRUCTURA DE DATOS
spellingShingle ANALISIS DE FALLAS
JAVA
ESTRUCTURA DE DATOS
Galeotti, Juan Pablo
Rosner, Nicolás
López Pombo, Carlos G.
Frías, Marcelo
Analysis of invariants for efficient bounded verification
topic_facet ANALISIS DE FALLAS
JAVA
ESTRUCTURA DE DATOS
description "SAT-based bounded veri cation of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for speci cation 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 elds. Experiments show that the translations to propositional formulas require signi cantly less propositional variables, leading in the experiments we have carried out to an improvement on the e ciency of the analysis of orders of magnitude, compared to the non instrumented SAT-based analysis. We show that, in somecases, our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking or SMT-solving."
format Ponencias en Congresos
publishedVersion
author Galeotti, Juan Pablo
Rosner, Nicolás
López Pombo, Carlos G.
Frías, Marcelo
author_facet Galeotti, Juan Pablo
Rosner, Nicolás
López Pombo, Carlos G.
Frías, Marcelo
author_sort Galeotti, Juan Pablo
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
publishDate 2022
url http://ri.itba.edu.ar/handle/123456789/3891
work_keys_str_mv AT galeottijuanpablo analysisofinvariantsforefficientboundedverification
AT rosnernicolas analysisofinvariantsforefficientboundedverification
AT lopezpombocarlosg analysisofinvariantsforefficientboundedverification
AT friasmarcelo analysisofinvariantsforefficientboundedverification
_version_ 1765660700201451520

Ejemplares similares