Accession Number : ADA617018


Title :   Parallel Software Model Checking


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST


Personal Author(s) : Chaki, Sagar ; Gurfinkel, Arie ; Karimi, Derrick


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a617018.pdf


Report Date : 08 Jan 2015


Pagination or Media Count : 4


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.


Descriptors :   *COMPUTER PROGRAM VERIFICATION , ALGORITHMS


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE