Mostrar el registro sencillo del ítem
dc.contributor.author
Kampmann, Alexander
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
Zeller, Andreas
dc.date.available
2018-04-10T20:39:44Z
dc.date.issued
2014-07
dc.identifier.citation
Kampmann, Alexander; Galeotti, Juan Pablo; Zeller, Andreas; JTACO: Test Execution for Faster Bounded Verification; Springer; Lecture Notes in Computer Science; 8570; 7-2014; 134-141
dc.identifier.issn
0302-9743
dc.identifier.uri
http://hdl.handle.net/11336/41629
dc.description.abstract
In bounded program verification a finite set of execution traces is exhaustively checked in order to find violations to a given specification (i.e. errors). SAT-based bounded verifiers rely on SAT-Solvers as their back-end decision procedure, accounting for most of the execution time due to their exponential time complexity.
In this paper we sketch a novel approach to improve SAT-based bounded verification. As modern SAT-Solvers work by augmenting partial assignments, the key idea is to translate some of these partial assignments into JUnit test cases during the SAT-Solving process. If the execution of the generated test cases succeeds in finding an error, the SAT-Solver is promptly stopped.
We implemented our approach in JTACO, an extension to the TACO bounded verifier, and evaluate our prototype by verifying parameterized unit tests of several complex data structures.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
Springer
![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
Taco
dc.subject
Bounded Verification
dc.subject
Testing
dc.subject
Sat-Solving
dc.subject.classification
Ingeniería de Sistemas y Comunicaciones
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.subject.classification
Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la 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
INGENIERÍAS Y TECNOLOGÍAS
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.title
JTACO: Test Execution for Faster Bounded Verification
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
2017-12-29T14:19:00Z
dc.journal.volume
8570
dc.journal.pagination
134-141
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
Berlín
dc.description.fil
Fil: Kampmann, Alexander. Universitat Saarland; Alemania
dc.description.fil
Fil: Galeotti, Juan Pablo. Universitat Saarland; Alemania. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina
dc.description.fil
Fil: Zeller, Andreas. Universitat Saarland; Alemania
dc.journal.title
Lecture Notes in Computer Science
![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/978-3-319-09099-3_10
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/https://link.springer.com/chapter/10.1007%2F978-3-319-09099-3_10
Archivos asociados