JTACO: Test Execution for Faster Bounded Verification
- TAP 2014
by
Alexander Kampmann, Juan Pablo Galeotti, Andreas Zeller
TAP 2014: Proceedings of the 8th International Conference on Tests and Proofs, Pages 134-141, Lecture Notes in Computer Science, Volume 8570, Springer, July 2014.
ISBN: 978-3-319-09098-6
ISSN: 0302-9743
Digital Library via DOI: 10.1007/978-3-319-09099-3_10 - Local copy: Download as PDF file.
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.
BibTeX Entry
@inproceedings{kampmann-tap-2014,
title = "JTACO: Test Execution for Faster Bounded Verification",
author = "Alexander Kampmann and Juan Pablo Galeotti and Andreas Zeller",
year = "2014",
month = jul,
booktitle = "TAP 2014: Proceedings of the 8th International Conference on Tests and Proofs",
location = "York, UK",
pages = "134--141",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = "8570",
ISBN = "978-3-319-09098-6",
ISSN = "0302-9743",
doi = "10.1007/978-3-319-09099-3_10",
}