Name
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2483760.2483770 | ISSTA |
Keywords | Field | DocType |
sequential analysis tool,commodity cluster hardware,novel technique,rich class invariants,rich invariants,disjoint subproblems,java code,java class field,original analysis,efficient bug-finding,automated parallel,parallel bounded analysis,field bound,static analysis | Disjoint sets,Computer science,Static analysis,Algorithm,Theoretical computer science,Invariant (mathematics),Soundness,Java,Completeness (statistics),Bounded function,Bounding overwatch | Conference |
Citations | PageRank | References |
4 | 0.41 | 26 |
Authors | ||
8 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nicolás Rosner | 1 | 68 | 5.14 |
| Juan P. Galeotti | 2 | 166 | 9.64 |
| Santiago Bermúdez | 3 | 4 | 0.41 |
| Guido Marucci Blas | 4 | 4 | 0.41 |
| Santiago Perez De Rosso | 5 | 18 | 1.50 |
| Lucas Pizzagalli | 6 | 4 | 0.41 |
| Luciano Zemín | 7 | 6 | 0.78 |
| Marcelo F. Frias | 8 | 295 | 35.57 |