抽取謂詞以改進性質導向可達性技術

Abstract

自從在2011年被提出後，性質導向可達性技術至今仍是最好的模型檢查演算法。但是仍有許多的案例是性質導向可達性技術難以解決的，因此，為了改進這個演算法，有許多的研究先後被發表。在這篇論文中，我們藉由獨立的檢查謂詞以輔助性質導向可達性演算法。此外，作為證明的例子，我們也提供了兩種能夠輕易從演算過程中得出的樣式。原本的性質導向可達性演算法與新方法皆被實作於Ia2b這個自製的模型檢查環境上。透過利用硬體模型檢查比賽的資料所做的實驗得知，我們所提出的方法能夠解出比原本的性質導向可達性技術更多的案例。

Since proposed in 2011, PDR (IC3) has been the best model checking algorithm until now. However, there are still many cases that PDR struggles to solve. Hence, many works are presented to enhance the algorithm. In this thesis, we propose a general method to aid PDR by solving predicate separately. Furthermore, we provide two kinds of useful pattern easily recognized from the solving process as example. The original PDR algorithm and the new feature are implemented on a custom model checking environment called Ia2b. The experiment on HWMCC benchmarks shows that our method can solve more cases than the classic PDR.