語系:
繁體中文
English
說明(常見問題)
回圖書館首頁
手機版館藏查詢
登入
回首頁
切換:
標籤
|
MARC模式
|
ISBD
Scaling Verification by Leveraging P...
~
Sethi, Divjyot.
FindBook
Google Book
Amazon
博客來
Scaling Verification by Leveraging Parametrization.
紀錄類型:
書目-電子資源 : Monograph/item
正題名/作者:
Scaling Verification by Leveraging Parametrization./
作者:
Sethi, Divjyot.
面頁冊數:
154 p.
附註:
Source: Dissertation Abstracts International, Volume: 76-04(E), Section: B.
Contained By:
Dissertation Abstracts International76-04B(E).
標題:
Engineering, Computer. -
電子資源:
http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3665345
ISBN:
9781321377224
Scaling Verification by Leveraging Parametrization.
Sethi, Divjyot.
Scaling Verification by Leveraging Parametrization.
- 154 p.
Source: Dissertation Abstracts International, Volume: 76-04(E), Section: B.
Thesis (Ph.D.)--Princeton University, 2014.
This item must not be sold to any third party vendors.
Modern hardware and software systems have become increasingly concurrent for increased performance. This performance, however, comes at a cost--these systems are highly error prone and hard to verify. Consequently, important techniques such as testing which have had considerable success in verifying sequential systems, have only witnessed limited success in verifying concurrent systems. These techniques can easily end up missing out important system bugs. In response, model checking has emerged as an important technique for exhaustively verifying such systems. Model checking verifies a model of the system by exhaustively exploring all the possible states the system can reach. However, this exhaustiveness comes at the cost of scalability: the system state which model checking has to explore grows exponentially with the system size. This is referred to as the state space explosion problem.
ISBN: 9781321377224Subjects--Topical Terms:
1669061
Engineering, Computer.
Scaling Verification by Leveraging Parametrization.
LDR
:03383nmm a2200313 4500
001
2056418
005
20150526083652.5
008
170521s2014 ||||||||||||||||| ||eng d
020
$a
9781321377224
035
$a
(MiAaPQ)AAI3665345
035
$a
AAI3665345
040
$a
MiAaPQ
$c
MiAaPQ
100
1
$a
Sethi, Divjyot.
$3
3170168
245
1 0
$a
Scaling Verification by Leveraging Parametrization.
300
$a
154 p.
500
$a
Source: Dissertation Abstracts International, Volume: 76-04(E), Section: B.
500
$a
Adviser: Sharad Malik.
502
$a
Thesis (Ph.D.)--Princeton University, 2014.
506
$a
This item must not be sold to any third party vendors.
520
$a
Modern hardware and software systems have become increasingly concurrent for increased performance. This performance, however, comes at a cost--these systems are highly error prone and hard to verify. Consequently, important techniques such as testing which have had considerable success in verifying sequential systems, have only witnessed limited success in verifying concurrent systems. These techniques can easily end up missing out important system bugs. In response, model checking has emerged as an important technique for exhaustively verifying such systems. Model checking verifies a model of the system by exhaustively exploring all the possible states the system can reach. However, this exhaustiveness comes at the cost of scalability: the system state which model checking has to explore grows exponentially with the system size. This is referred to as the state space explosion problem.
520
$a
In this dissertation, I propose techniques for scaling model checking to large concurrent systems. In particular, I focus on systems which use simple replicated components operating concurrently in order to achieve high performance. Examples of such systems include multi-threaded software, multi-processors and data centers. In order to scale verification to a large number of components, I leverage special mathematical representations of these systems, referred to as parameterized systems. Verification techniques for these systems, i.e., parameterized verification techniques, verify them for an unbounded number of components operating concurrently. These techniques typically work by constructing small-sized, over-approximate models of the system. This is accomplished by iteratively using abstraction and refinement techniques, where the abstraction technique typically reduces the size of the model under verification by discarding information and the refinement technique typically adds back any information required, which got discarded by the abstraction technique.
520
$a
The parametric verification techniques developed in this dissertation either (1) rewrite the property under verification in order to enable efficient existing abstractions, (2) construct novel abstractions, or (3) construct novel refinement mechanisms. Using these techniques, I have verified systems from three important application domains: cache coherence protocols, emerging computer networks (software defined networks), and concurrent data structures.
590
$a
School code: 0181.
650
4
$a
Engineering, Computer.
$3
1669061
650
4
$a
Computer Science.
$3
626642
690
$a
0464
690
$a
0984
710
2
$a
Princeton University.
$b
Electrical Engineering.
$3
2095953
773
0
$t
Dissertation Abstracts International
$g
76-04B(E).
790
$a
0181
791
$a
Ph.D.
792
$a
2014
793
$a
English
856
4 0
$u
http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3665345
筆 0 讀者評論
館藏地:
全部
電子資源
出版年:
卷號:
館藏
1 筆 • 頁數 1 •
1
條碼號
典藏地名稱
館藏流通類別
資料類型
索書號
使用類型
借閱狀態
預約狀態
備註欄
附件
W9288907
電子資源
11.線上閱覽_V
電子書
EB
一般使用(Normal)
在架
0
1 筆 • 頁數 1 •
1
多媒體
評論
新增評論
分享你的心得
Export
取書館
處理中
...
變更密碼
登入