Parallel Bounded Analysis in Code with Rich Invariants by Refinement of Field Bounds

ROSNER, NICOLÁS; GALEOTTI, JUAN PABLO; BERMÚDEZ, SANTIAGO; MARUCCI BLAS, GUIDO; PEREZ DE ROSSO, SANTIAGO; PIZZAGALLI, LUCAS; ZEMÍN, LUCIANO; FRIAS, MARCELO FABIAN

Lugano

Simposio; International Symposium on Software Testing and Analysis, ISSTA '13; 2013

Association for Computing Machinery

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 gen- erally 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 imple- ments this technique, yields significant speed-ups over TACO on commodity cluster hardware.