Artículo
JTACO: Test Execution for Faster Bounded Verification
Fecha de publicación:
07/2014
Editorial:
Springer
Revista:
Lecture Notes in Computer Science
ISSN:
0302-9743
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
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.
Palabras clave:
Taco
,
Bounded Verification
,
Testing
,
Sat-Solving
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(OCA CIUDAD UNIVERSITARIA)
Articulos de OFICINA DE COORDINACION ADMINISTRATIVA CIUDAD UNIVERSITARIA
Articulos de OFICINA DE COORDINACION ADMINISTRATIVA CIUDAD UNIVERSITARIA
Citación
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
Compartir
Altmétricas