We introduce a structure-aware parallel technique for context-bounded analysis of concurrent programs. The key intuition consists in decomposing the set of concurrent traces into symbolic subsets that are separately explored by multiple instances of the same decision procedure running in parallel. Since the decision procedures work on different partitions of the search space without cooperating, distribution follows effortlessly. Our experiments on a selection of complex multi-threaded programs show significant analysis speedups and scalability, and greater performance gains than with general-purpose parallel solvers.

Artefact for PPoPP 2020 paper (https://doi.org/10.1145/3332466.3374529). Work partially funded by MIUR projects PRIN 2017FTXR7S IT MATTERS (Methods and Tools for Trustworthy Smart Systems) and PRIN 2017TWRCNB SEDUCE (Designing Spatially Distributed Cyber-Physical Systems under Uncertainty).