Name
Abstract | ||
|---|---|---|
While directed model checking has proven to be a powerful tool in the fight against concurrency bugs, scalability remains a concern due to the combinatorial explosion in size of the state space. Overcoming that combinatorial explosion requires the selection and/or parameterization of meta*-heuristics, but we are left with a persistent problem of having to provide or compute specialized knowledge of the program under consideration, and this limits the practical value of the technique. To circumvent that, this paper investigates directed model checking as a platform for the synthesis of results from other analyses. We introduce an open-source tool, Ariadne, which translates reports of suspected race conditions of a static analyzer (Petablox) to instrumentation using a source-to-source compiler (ROSE) that can be exploited by a model checker (Java Pathfinder). We detail the algorithm used, present experimental results, and outline directions for future research. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/ICST.2017.49 | 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST) |
Keywords | Field | DocType |
model checking,heuristics,static analysis,race detection | Programming language,Model checking,Concurrency,Computer science,Software bug,Static analysis,Compiler,Real-time computing,State space,Combinatorial explosion,Scalability | Conference |
ISSN | ISBN | Citations |
2381-2834 | 978-1-5090-6032-0 | 1 |
PageRank | References | Authors |
0.36 | 16 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Reed Milewicz | 1 | 8 | 2.47 |
| Peter Pirkelbauer | 2 | 52 | 9.37 |