東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Scaling Verification by Leveraging P...

Sethi, Divjyot.

Linked to FindBook

Google Book

Amazon

博客來

Scaling Verification by Leveraging Parametrization.

Record Type:	Electronic resources : Monograph/item
Title/Author:	Scaling Verification by Leveraging Parametrization./
Author:	Sethi, Divjyot.
Description:	154 p.
Notes:	Source: Dissertation Abstracts International, Volume: 76-04(E), Section: B.
Contained By:	Dissertation Abstracts International76-04B(E).
Subject:	Engineering, Computer. -
Online resource:	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