Abstract

By exhaustively exploring all possible behaviours of the system, model checking has to face the state space explosion problem. We target the verification of concurrent programs. Dynamic partial-order reduction (DPOR), is a mature approach to mitigate the state explosion problem based on Mazurkiewicz trace theory, whereas unfolding is still at an initial state for targetting programs.

We propose to combine DPOR and unfolding into an algorithm called Unfolding based POR. In order to obtain optimality, the algorithm is forced to compute sequences of transitions known as alternatives.

In this thesis, we prove that computing alternatives in optimal DPOR is an NP-complete problem. As a trade-off solution, we propose a hybrid approach called Quasi-Optimal POR (QPOR). In particular, we provide a new notion of k-partial alternative and a polynomial algorithm to compute alternative executions.

Another main algorithmic contribution is to represent causality and conflict as a set of trees where events are encoded as one or two nodes in two different trees. We show that checking causality and conflict between events amounts to an efficient traversal in one of these trees. We also implement the algorithm and data structures in a new tool. Besides the algorithmic improvements guaranteed by QPOR, parallelization is another way to speed up the unfolding exploration, thus we propose a parallel algorithm based on parallelizing QPOR.

Finally, we conduct experiments on the sequential implementation of QPOR and compare the results with other state-of-art testing and verification tools to evaluate the efficiency of our algorithms. The analysis shows that our tool outperforms them.

 Ảnh 1: Trình bày kết quả luận án trước hội đồng

 Ảnh 2: Chụp ảnh với các GS trong hội đồng sau khi bảo vệ thành công luận án