利用非滿足性核心所建構之抽象化轉移關係進行無界模型檢驗

Constructing Abstract Transition Relation by UNSAT Core for Unbounded Model Checking

賴建宇(Chien-Yu Lai)

指導教授 ： 黃鐘揚

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2013年)

https://doi.org/10.6342/NTU.2013.10729

摘要

內插模型檢驗是一種無界模型驗證演算法。在內插模型檢驗之中，抽象修正是很困難的。事實上，在McMillan內插模型檢驗與NewITP兩個之前的演算法中，抽象修正效果不是很彰顯。傳統的McMillan內插模型檢驗在遇到反例的時候只是修正了有界模型檢驗的步數。已經計算的內插函數對於未來的迭代中是沒有幫助的。NewITP除了修正了有界模型檢驗的步數之外，還從通用化的方塊中排除了之前遇到的反例。然而排除之前遇到的反例只是排除一些最小項來修正抽象。當一個問題傾向於在NewITP演算法中產生許多的反例，詳細地排除布林空間過於昂貴以致於不實用。共通的問題在於固定的抽象粒度。只有固定抽象粒度，抽象只會適合相對應的檢驗問題。在這篇論文之中，有三個新的特徵被提出。第一，我們提倡抽象程度應該要隨著輸入的問題調整，並且提出一個可調性的內插模型檢驗。第二，為了建立適合輸入的問題的抽象，我們提出了抽象調控演算法，稱為利用切割可達度達成彈性內插。第三，我們提出一個新的內插引擎，抽象轉移關係與可達度兩段式內插，是一個可以跟我們提出的第二項特徵相結合的內插引擎。實驗結果顯示我們的可調式內插模型檢驗，與之前的研究相比，解出最多的問題，因為我們的可調度調整個抽象層次並且找到適合輸入問題的抽象值。

關鍵字

內插 ； 無界模型檢驗

並列摘要

Interpolation-based model checking (IMC) is an unbounded model checking algorithm. Refinement in IMC is difficult. In fact, refinements of both previous works, McMillan’s IMC or NewITP, are not quite effective. Traditional McMillan’s IMC refines BMC step when a spurious counter-examples is found. The computed interpolant does no help for the future iterations. In addition to refining BMC step, NewITP prunes the states of previously encountered spurious counter-examples from generalized cubes. However, pruning those counter-examples only refines the abstraction by excluding some minterms from the interpolant. When an instance tends to produce many counter-examples in NewITP, exhaustively pruning the Boolean space is too expensive to be practical. The common problem of previous works is the fixed granularities of the interpolation engine. With fixed granularity, the abstraction is only adequate for corresponding instances. In this paper, three new features are proposed. First, we suggest that the abstraction degree should be adjusted with an input problem, and we propose an adaptive IMC. Second, to construct abstraction suited for an input problem, we propose an abstraction manipulation algorithm, called flexible interpolation by reachability partitioning. Third, we propose a new interpolation engine, ATR&R 2-phase interpolation, which can be manipulated by our second feature. The experimental results show that our adaptive IMC solves the most instances compared with previous works because the adaptivity adjusts the abstraction degree and find the adequate abstraction.

並列關鍵字

interpolation ； unbounded model checking

參考文獻

[1] K. McMillan. Interpolation and sat-based model checking. In Computer Aided Verification, pages 113. Springer, 2003.

[2] C.Y. Wu, C.A. Wu, C.Y. Lai, and C.Y. Huang, A Counterexample-Guided Interpolant Generation Algorithm for SAT-based Model Checking. In 50th Design Automation Conference, IEEE 2013.

[3] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without bdds. Tools and Algorithms for the Construction and Analysis of Systems, pages 193-207, 1999.

[4] W. Craig. Linear reasoning: A new form of the herbrand-gentzen theorem. Journal of Symbolic Logic, pages 250-268, 1957.

[5] P. Pudlak. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic, pages 981-998, 1997.