Analysis of invariants for efficient bounded verification

Galeotti, Juan Pablo; Rosner, Nicolás; López Pombo, Carlos G.; Frías, Marcelo

ponencia en congreso.page.titleprefix
Analysis of invariants for efficient bounded verification

dc.contributor.author	Galeotti, Juan Pablo
dc.contributor.author	Rosner, Nicolás
dc.contributor.author	López Pombo, Carlos G.
dc.contributor.author	Frías, Marcelo
dc.date.accessioned	2022-05-23T18:51:29Z
dc.date.available	2022-05-23T18:51:29Z
dc.date.issued	2010-07
dc.description.abstract	"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."	en
dc.identifier.uri	http://ri.itba.edu.ar/handle/123456789/3891
dc.language.iso	en	en
dc.relation	info:eu-repo/semantics/altIdentifier/doi/10.1145/1831708.1831712
dc.subject	ANALISIS DE FALLAS	es
dc.subject	JAVA	es
dc.subject	ESTRUCTURA DE DATOS	es
dc.title	Analysis of invariants for efficient bounded verification	en
dc.type	Ponencias en Congresos	es
dc.type	info:eu-repo/semantics/publishedVersion
dspace.entity.type	Ponencia en Congreso
itba.description.filiation	Fil: Galeotti, Juan Pablo. Universidad de Buenos Aires; Argentina.
itba.description.filiation	Fil: Rosner, Nicolás. Universidad de Buenos Aires; Argentina.
itba.description.filiation	Fil: López Pombo, Carlos G. Universidad Nacional de Buenos Aires; Argentina.
itba.description.filiation	Fil: Frías, Marcelo. Instituto Tecnológico de Buenos Aires; Argentina.