Parallel Software Model Checking
Abstract
As the DoD continues to become software reliant, rigorous techniques to assure the correct behavior of programs are in great demand. Software model checking (SMC) is a promising candidate, but its scalability remains unsatisfactory. Recent years have seen the emergence of HPC technologies, e.g., multi-core processors and clusters. Yet, few software model checkers are designed to use this cheap and abundant computing power. A key reason is that model checking is at its core a graph search -- where the graph is the state-space of the model -- which is difficult to parallelize effectively (i.e., obtain reasonable speedups). The main challenge is to partition the search among the CPUs in a way that limits duplicated effort and communication bottlenecks. A promising approach is to start with a verification algorithm that maintains a "worklist" and to distribute elements of the worklist to different CPUs in a "balanced" manner. New elements are added to the worklist as a result of processing an existing element. For example, this strategy has been used successfully to parallelize the breadth-first-search in the SPIN model checker. This project will explore this strategy to parallelize the generalized PDR algorithm for software model checking. It belongs to TF1 due to its focus on formal verification.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 08, 2015
- Accession Number
- ADA617018
Entities
People
- Arie Gurfinkel
- Derrick Karimi
- Sagar Chaki
Organizations
- Carnegie Mellon University