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",
}

Show all publications of the Software Engineering Chair.