Software has a central role in modern society: Almost all of today's 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. This project addresses 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.
This project is being funded by SNF
