Harnessing Parallel Computing for Model Checking

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 increasing 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.