Parallel Bounded Analysis in Code with Rich Invariants by Refinement of Field Bounds
- ISSTA 2013
by
Nicolas Rosner, Juan Pablo Galeotti, Santiago Bermudez, Guido Marucci Blas, Santiago Perez De Rosso, Lucas Pizzagalli, Luciano Zemin, Marcelo F. Frias
ISSTA '13: Proceedings of the 2013 International Symposium on Software Testing and Analysis, July 2013.
Digital Library via DOI: 10.1145/2483760.2483770 - Local copy: Download as PDF file.
Abstract
In this article we present a novel technique for automated parallel bug-finding based on the sequential analysis tool TACO. TACO is a tool based on SAT-solving for efficient bug-finding in Java code with rich class invariants. It prunes the SAT-solver's search space by introducing precise symmetry-breaking predicates and bounding the relational semantics of Java class fields. The bounds computed by TACO generally include a substantial amount of nondeterminism; its reduction allows us to split the original analysis into disjoint subproblems. We discuss the soundness and completeness of the decomposition. Furthermore, we present experimental results showing that MUCHO-TACO, our tool which implements this technique, yields significant speed-ups over TACO on commodity cluster hardware.
BibTeX Entry
@inproceedings{rosner-issta-2013,
title = "Parallel Bounded Analysis in Code with Rich Invariants by Refinement of Field Bounds",
author = "Nicolas Rosner and Juan Pablo Galeotti and Santiago Bermudez and Guido Marucci Blas and Santiago Perez De
Rosso and Lucas Pizzagalli and Luciano Zemin and Marcelo F. Frias",
year = "2013",
month = jul,
booktitle = "ISSTA '13: Proceedings of the 2013 International Symposium on Software Testing and Analysis",
location = "Lugano, Switzerland",
doi = "10.1145/2483760.2483770",
}