Mostrar el registro sencillo del ítem
dc.contributor.author
Cuervo Parrino, Bruno
dc.contributor.author
Galeotti, Juan Pablo
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.contributor.author
Garbervetsky, Diego David
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.contributor.author
Frias, Marcelo Fabian
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.date.available
2018-03-02T20:23:09Z
dc.date.issued
2015-01
dc.identifier.citation
Cuervo Parrino, Bruno; Galeotti, Juan Pablo; Garbervetsky, Diego David; Frias, Marcelo Fabian; TacoFlow: optimizing SAT program verification using dataflow analysis; Springer Heidelberg; Software and Systems Modeling; 14; 1; 1-2015; 45-63
dc.identifier.issn
1619-1366
dc.identifier.uri
http://hdl.handle.net/11336/37732
dc.description.abstract
In previous work, we presented TACO, a tool for efficient bounded verification. TACO translates programs annotated with contracts to a SAT problem which is then solved resorting to off-the-shelf SAT-solvers. TACO may deem propositional variables used in the description of a program initial states as being unnecessary. Since the worst-case complexity of SAT (a known NP problem) depends on the number of variables, most times this allows us to obtain significant speed ups. In this article, we present TacoFlow, an improvement over TACO that uses dataflow analysis in order to also discard propositional variables that describe intermediate program states. We present an extensive empirical evaluation that considers the effect of removing those variables at different levels of abstraction, and a discussion on the benefits of the proposed approach.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
Springer Heidelberg
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.rights
info:eu-repo/semantics/openAccess
dc.rights.uri
https://creativecommons.org/licenses/by-nc-sa/2.5/ar/
dc.subject
Dataflow Analysis
dc.subject
Java-Like Programs Verification
dc.subject
Sat-Based Verification
dc.subject.classification
Ciencias de la Computación
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.subject.classification
Ciencias de la Computación e Información
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.subject.classification
CIENCIAS NATURALES Y EXACTAS
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.title
TacoFlow: optimizing SAT program verification using dataflow analysis
dc.type
info:eu-repo/semantics/article
dc.type
info:ar-repo/semantics/artículo
dc.type
info:eu-repo/semantics/publishedVersion
dc.date.updated
2018-03-02T14:00:47Z
dc.journal.volume
14
dc.journal.number
1
dc.journal.pagination
45-63
dc.journal.pais
Alemania
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.journal.ciudad
Heidelberg
dc.description.fil
Fil: Cuervo Parrino, Bruno. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina
dc.description.fil
Fil: Galeotti, Juan Pablo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Universitat Saarland; Alemania
dc.description.fil
Fil: Garbervetsky, Diego David. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina
dc.description.fil
Fil: Frias, Marcelo Fabian. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Instituto Tecnológico de Buenos Aires. Facultad de Ingeniería. Departamento de Informática; Argentina
dc.journal.title
Software and Systems Modeling
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/doi/http://dx.doi.org/10.1007/s10270-014-0401-9
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/https://link.springer.com/article/10.1007%2Fs10270-014-0401-9
Archivos asociados