From Parallel SMT to Parallel Software Verification

This proposal describes a request of extension to the SNF funded project #153402 on Harnessing Parallel Computing for Model Checking running now on its second year. The first year of the project resulted in a publication in SAT 2015, a premier conference in constraint solving, and the first cloud-based and multithreaded implementations of a parallel SMT solver using novel paralellization strategies and search space partitioning. The results so far confirm the viability of the ideas presented in the original proposal. We have found the experience obtained in the process extremely useful in further strengthening the continuation outlined already in the first proposal. Since the original proposal was funded only partially we have made certain adjustments to the extension, reformulating some of the goals for this proposal. Software has a central role in modern society: Almost all of todays industry depends critically on software either directly in the products or indirectly during the production, and the safety, cost-efficiency and environmentally friendliness of infrastructure, including the electric grid, public transportation, and health care, rely increasingly on correctly working software. The growing role of software in society means that the consequences of software faults can be catastrophic, and as a result proving the correctness of software is widely thought to be one of the most central challenges for computer science, the related work having been acknowledged with prestigious recognitions such as the Turing award. Verifying complex software can be extremely expensive. We propose to address the challenges of software verification with an extensive parallel model checking framework able to scale to the massive amounts of processing power offered by computing clouds. We will use the framework to study the parallelization of key aspects of model checking, including the underlying SMT solver used as a reasoning engine, model-checking algorithms, and widely applicable related technologies such as interpolation. The results of the framework will be used in two flagship applications, a parallel SMT solver, and a parallel software model checker. We expect the research to improve the current state-of-the-art not only in model checking, but also in other applications where constraint solving has been successful.