Ponencia en Congreso:
Analysis of invariants for efficient bounded verification

dc.contributor.authorGaleotti, Juan Pablo
dc.contributor.authorRosner, Nicolás
dc.contributor.authorLópez Pombo, Carlos G.
dc.contributor.authorFrías, Marcelo
dc.date.accessioned2022-05-23T18:51:29Z
dc.date.available2022-05-23T18:51:29Z
dc.date.issued2010-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.urihttp://ri.itba.edu.ar/handle/123456789/3891
dc.language.isoenen
dc.relationinfo:eu-repo/semantics/altIdentifier/doi/10.1145/1831708.1831712
dc.subjectANALISIS DE FALLASes
dc.subjectJAVAes
dc.subjectESTRUCTURA DE DATOSes
dc.titleAnalysis of invariants for efficient bounded verificationen
dc.typePonencias en Congresoses
dc.typeinfo:eu-repo/semantics/publishedVersion
dspace.entity.typePonencia en Congreso
itba.description.filiationFil: Galeotti, Juan Pablo. Universidad de Buenos Aires; Argentina.
itba.description.filiationFil: Rosner, Nicolás. Universidad de Buenos Aires; Argentina.
itba.description.filiationFil: López Pombo, Carlos G. Universidad Nacional de Buenos Aires; Argentina.
itba.description.filiationFil: Frías, Marcelo. Instituto Tecnológico de Buenos Aires; Argentina.

Archivos

Bloque original
Mostrando 1 - 1 de 1
Cargando...
Miniatura
Nombre:
Galeotti_Rossner_2010_ING_INFORMATICA_ponencia.pdf
Tamaño:
553.63 KB
Formato:
Adobe Portable Document Format
Descripción:
Ponencia_Galeotti
Bloque de licencias
Mostrando 1 - 1 de 1
No hay miniatura disponible
Nombre:
license.txt
Tamaño:
1.6 KB
Formato:
Item-specific license agreed upon to submission
Descripción: