Cô Nguyễn Thị Thanh Huyền bảo vệ thành công luận án Tiến sĩ

Ngày 21 tháng 12 năm 2018, tại Trường Đại học Paris 13, cô Nguyễn Thị Thanh Huyền, giảng viên bộ môn Công nghệ phần mềm, Khoa CNTT, ĐHSPHN đã bảo vệ thành công luận án Tiến sĩ trong lĩnh vực công nghệ phần mềm với tiêu đề "Quasi Optimal model checking for concurrent systems". 

Dưới đây là tóm tắt luận án và một số hình ảnh trong buổi lễ bảo vệ.


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