東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Incremental, Inductive Model Checking.

Hassan, Zyad.

Linked to FindBook

Google Book

Amazon

博客來

Incremental, Inductive Model Checking.

Record Type:	Electronic resources : Monograph/item
Title/Author:	Incremental, Inductive Model Checking./
Author:	Hassan, Zyad.
Description:	107 p.
Notes:	Source: Dissertation Abstracts International, Volume: 75-09(E), Section: B.
Contained By:	Dissertation Abstracts International75-09B(E).
Subject:	Engineering, Computer. -
Online resource:	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