利用動態時間框架延展增進性質導向可達性技術

Abstract

性質導向可達性技術自從在2011年被發表之後，一直是最有效率的模型驗證演算法。不像其他的演算法往往只偏向於安全或不安全的案例其中一者，性質導向可達性技術對於兩者都能有不錯的效能。然而，仍然有些案例是難以被解決的，所以一直有對於如何改進性質導向可達性技術的研究。在這篇論文中，我們提出了兩種將有界模型驗證融合進性質導向可達性技術的方法，以及一種結合原本的性質導向可達性技術和以上兩種演算法的混合演算法。我們在V3的框架上實做了我們的演算法，並用硬體模型驗證競賽的案例進行測試。實驗結果指出我們的演算法可以在較短的時間內解出比原本的演算法還多的案例。

Property Directed Reachability (PDR) has been the most efficient model checking algorithm since its publication in 2011. Unlike other algorithms which often prefers either SAT cases (bug finders) or UNSAT cases (prover), PDR is well balanced that it can solve both categories efficiently. However, there are still some hard cases that PDR fails to solve, so researchers keep finding ways to improve PDR. In this thesis, we propose two modifications that integrate the idea of bounded model checking (BMC) into PDR, and a hybrid version that combines those two methods with original PDR. We implement the algorithms on V3 framework and test the performance using HWMCC benchmarks. Experiment shows that our algorithm can solve more cases than the original PDR algorithm with less average runtime.