Parallel computational tree logic model-checking on pushdown systems

Model checking and static analysis have been well studied for program verification. Because of the ability to describe the stack, the pushdown system (PDS) has become a perfect model that is able to accurately model procedure calls and mimic the program's stack. Thus, it is not only a good model for sequential programs but for malware detection as well. However, with the increase of the complexity of programs, the size of models becomes huge as well. Thus, the model-checking problem is expensive to solve. The computational tree logic (CTL) is a widely used logic and its model checking problem of PDSs can be reduced to the emptiness analysis of an alternating Buchi pushdown system (ABPDS) by determining whether there is an accepting run. When the size of a PDS is huge, the computations can be time-consuming. To overcome this limitation, we propose a parallel solution. We propose a parallel framework based on the Compute Unified Device Architecture and the corresponding parallel algorithms to solve the emptiness problem of ABPDSs. Moreover, in order to effectively utilize the graphics processing unit, we design a new data structure of variables and an algorithm of management of thread scheduling for the parallel model. We implement our algorithms in a tool and compare our tool to a CTL model checker for PDS as a benchmark. The comparison results indicate an encouraging performance speedup.