請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/17162
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚 | |
dc.contributor.author | Chien-Yu Lai | en |
dc.contributor.author | 賴建宇 | zh_TW |
dc.date.accessioned | 2021-06-07T23:59:04Z | - |
dc.date.copyright | 2013-08-28 | |
dc.date.issued | 2013 | |
dc.date.submitted | 2013-08-16 | |
dc.identifier.citation | [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. [6] M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a sat-solver. In Formal Methods in Computer-Aided Design, pages 127-144. Springer, 2000. [7] N. Een, A. Mishchenko, and R. Brayton. Efficient implementation of property directed reachability. In Formal Methods in Computer-Aided Design (FMCAD), 2011, pages 125-134. IEEE, 2011. [8] A. Bradley. Sat-based model checking without unrolling. In Verification, Model Checking, and Abstract Interpretation, pages 70-87. Springer, 2011. [9] G. S. Tseitin. On the complexity of derivation in propositional calculus. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pages 46-{483, Springer, Berlin, Heidelberg, 1983. [10] Hardware Model Checking Competition. http://fmv.jku.at/hwmcc/. [11] N. Een and N. Sorensson. An extensible sat-solver. In Theory and Applications of Satisability Testing, pages 333-336. Springer, 2004. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/17162 | - |
dc.description.abstract | 內插模型檢驗是一種無界模型驗證演算法。在內插模型檢驗之中,抽象修正是很困難的。事實上,在McMillan內插模型檢驗與NewITP兩個之前的演算法中,抽象修正效果不是很彰顯。傳統的McMillan內插模型檢驗在遇到反例的時候只是修正了有界模型檢驗的步數。已經計算的內插函數對於未來的迭代中是沒有幫助的。NewITP除了修正了有界模型檢驗的步數之外,還從通用化的方塊中排除了之前遇到的反例。然而排除之前遇到的反例只是排除一些最小項來修正抽象。當一個問題傾向於在NewITP演算法中產生許多的反例,詳細地排除布林空間過於昂貴以致於不實用。共通的問題在於固定的抽象粒度。只有固定抽象粒度,抽象只會適合相對應的檢驗問題。在這篇論文之中,有三個新的特徵被提出。第一,我們提倡抽象程度應該要隨著輸入的問題調整,並且提出一個可調性的內插模型檢驗。第二,為了建立適合輸入的問題的抽象,我們提出了抽象調控演算法,稱為利用切割可達度達成彈性內插。第三,我們提出一個新的內插引擎,抽象轉移關係與可達度兩段式內插,是一個可以跟我們提出的第二項特徵相結合的內插引擎。實驗結果顯示我們的可調式內插模型檢驗,與之前的研究相比,解出最多的問題,因為我們的可調度調整個抽象層次並且找到適合輸入問題的抽象值。 | zh_TW |
dc.description.abstract | 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. | en |
dc.description.provenance | Made available in DSpace on 2021-06-07T23:59:04Z (GMT). No. of bitstreams: 1 ntu-102-R00943091-1.pdf: 473216 bytes, checksum: 35b20365e0e6f8f52e0b74a73e83540f (MD5) Previous issue date: 2013 | en |
dc.description.tableofcontents | 誌謝 i
中文摘要 ii ABSTRACT iii CONTENTS iv LIST OF FIGURES vi LIST OF TABLES vii LIST OF ALGORITHMS viii Chapter 1 Introduction 1 Chapter 2 Preliminaries 6 2.1 Propositional Satifiability………. 6 2.2 Hardware Model Checking 6 2.2.1 K-Induction 6 2.2.2 Property-Directed Reachability 7 2.2.3 Interpolation-Based Model Checking 7 2.2.4 Comparisons 7 Chapter 3 Flexible Interpolation by Reachability Partitioning 9 3.1 Dependence of reachability coverage and its abstraction pre-image 9 3.2 Flexible Interpolation by Reachability Partitioning 10 3.3 Hardness of Co-operation with previous works 13 Chapter 4 Transition Relation Abstraction and ATR-Circuit 14 4.1 ATR Extraction 14 4.2 ATR Circuit & ATR Circuit Simulation 16 Chapter 5 From ATR to Interpolant 19 5.1 Preprocessing 19 5.2 States collection 21 5.3 Inductive Invariant 21 5.4 Collection Order Heuristic 21 5.5 Comparison with NewITP 22 Chapter 6 Adaptive IMC by ATR&R Interpolation 23 6.1 Abstraction Degree Evaluation 23 6.2 Adaptivity of IMC 25 6.3 Local Fine-Grained Collection 25 Chapter 7 Experimental Results 27 7.1 Comparison of Total Cases 27 7.2 Comparison of Cases Hard for PDR 30 Chapter 8 Conclusion 44 Reference 46 | |
dc.language.iso | en | |
dc.title | 利用非滿足性核心所建構之抽象化轉移關係進行無界模型檢驗 | zh_TW |
dc.title | Constructing Abstract Transition Relation by UNSAT Core for Unbounded Model Checking | en |
dc.type | Thesis | |
dc.date.schoolyear | 101-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 江介宏,李建模,顏嘉志 | |
dc.subject.keyword | 內插,無界模型檢驗, | zh_TW |
dc.subject.keyword | interpolation,unbounded model checking, | en |
dc.relation.page | 47 | |
dc.rights.note | 未授權 | |
dc.date.accepted | 2013-08-16 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-102-1.pdf 目前未授權公開取用 | 462.12 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。