語系:
繁體中文
English
說明(常見問題)
回圖書館首頁
手機版館藏查詢
登入
回首頁
切換:
標籤
|
MARC模式
|
ISBD
Incremental, Inductive Model Checking.
~
Hassan, Zyad.
FindBook
Google Book
Amazon
博客來
Incremental, Inductive Model Checking.
紀錄類型:
書目-電子資源 : Monograph/item
正題名/作者:
Incremental, Inductive Model Checking./
作者:
Hassan, Zyad.
面頁冊數:
107 p.
附註:
Source: Dissertation Abstracts International, Volume: 75-09(E), Section: B.
Contained By:
Dissertation Abstracts International75-09B(E).
標題:
Engineering, Computer. -
電子資源:
http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3621337
ISBN:
9781303923753
Incremental, Inductive Model Checking.
Hassan, Zyad.
Incremental, Inductive Model Checking.
- 107 p.
Source: Dissertation Abstracts International, Volume: 75-09(E), Section: B.
Thesis (Ph.D.)--University of Colorado at Boulder, 2014.
This item must not be sold to any third party vendors.
Model checking has become a widely adopted approach for the verification of hardware designs. The ever increasing complexity of these designs creates a continuous need for faster model checkers that are capable of verifying designs within reasonable time frames to reduce time to market. IC3, the recently developed, very successful algorithm for model checking safety properties, introduced a new approach to model checking: incremental, inductive verification (IIV). The IIV approach possesses several attractive traits, such as stability and not relying on high-effort reasoning, that make its usage in model checking very appealing, which motivated the development of another algorithm that follows the IIV approach for model checking o-regular languages. The algorithm, Fair, has been shown to be capable of dealing with designs beyond the reach of its predecessors.
ISBN: 9781303923753Subjects--Topical Terms:
1669061
Engineering, Computer.
Incremental, Inductive Model Checking.
LDR
:03222nmm a2200313 4500
001
2056248
005
20150505071906.5
008
170521s2014 ||||||||||||||||| ||eng d
020
$a
9781303923753
035
$a
(MiAaPQ)AAI3621337
035
$a
AAI3621337
040
$a
MiAaPQ
$c
MiAaPQ
100
1
$a
Hassan, Zyad.
$3
3169996
245
1 0
$a
Incremental, Inductive Model Checking.
300
$a
107 p.
500
$a
Source: Dissertation Abstracts International, Volume: 75-09(E), Section: B.
500
$a
Advisers: Fabio Somenzi; Aaron R. Bradley.
502
$a
Thesis (Ph.D.)--University of Colorado at Boulder, 2014.
506
$a
This item must not be sold to any third party vendors.
520
$a
Model checking has become a widely adopted approach for the verification of hardware designs. The ever increasing complexity of these designs creates a continuous need for faster model checkers that are capable of verifying designs within reasonable time frames to reduce time to market. IC3, the recently developed, very successful algorithm for model checking safety properties, introduced a new approach to model checking: incremental, inductive verification (IIV). The IIV approach possesses several attractive traits, such as stability and not relying on high-effort reasoning, that make its usage in model checking very appealing, which motivated the development of another algorithm that follows the IIV approach for model checking o-regular languages. The algorithm, Fair, has been shown to be capable of dealing with designs beyond the reach of its predecessors.
520
$a
This thesis explores IIV as a promising approach to model checking. After identifying IIV's main elements, the thesis presents an IIV-based model checking algorithm for CTL: the first practical SAT-based algorithm for branching time properties. The algorithm, IICTL, is shown to complement state-of-the-art BDD-based CTL algorithms on a large set of benchmarks. In addition to fulfilling the need for a SAT-based CTL algorithm, IICTL highlights ways in which IIV algorithms can be improved; one of these ways is addressing counterexamples to generalization, which is explored in the context of IC3 and is shown to improve the algorithm's performance considerably. The thesis then addresses an important question: for properties that fall into the scope of more than one IIV algorithm, do these algorithms behave identically? The question is answered negatively, pointing out that the IIV framework admits multiple strategies and that there is a wide spectrum of possible algorithms that all follow the IIV approach. For example, all properties in the common fragment of LTL and CTL---an important class of properties---can be checked with Fair and IICTL. However, empirical evidence presented in the thesis suggests that neither algorithm is always superior to the other, which points out the importance of being flexible in deciding the strategy to apply to a given problem.
590
$a
School code: 0051.
650
4
$a
Engineering, Computer.
$3
1669061
650
4
$a
Computer Science.
$3
626642
650
4
$a
Engineering, General.
$3
1020744
690
$a
0464
690
$a
0984
690
$a
0537
710
2
$a
University of Colorado at Boulder.
$b
Electrical Engineering.
$3
1025672
773
0
$t
Dissertation Abstracts International
$g
75-09B(E).
790
$a
0051
791
$a
Ph.D.
792
$a
2014
793
$a
English
856
4 0
$u
http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3621337
筆 0 讀者評論
館藏地:
全部
電子資源
出版年:
卷號:
館藏
1 筆 • 頁數 1 •
1
條碼號
典藏地名稱
館藏流通類別
資料類型
索書號
使用類型
借閱狀態
預約狀態
備註欄
附件
W9288727
電子資源
11.線上閱覽_V
電子書
EB
一般使用(Normal)
在架
0
1 筆 • 頁數 1 •
1
多媒體
評論
新增評論
分享你的心得
Export
取書館
處理中
...
變更密碼
登入