About: Efficient Large-Scale Model Checking

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Efficient Large-Scale Model Checking Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	Model checking is a popular technique to systematically and automatically verify system properties. Unfortunately, the well-known state explosion problem often limits the extent to which it can be applied to realistic specifications, due to the huge resulting memory requirements. Distributed-memory model checkers exist, but have thus far only been evaluated on small-scale clusters, with mixed results. We examine one well-known distributed model checker, DiVinE, in detail, and show how a number of additional optimizations in its runtime system enable it to efficiently check very demanding problem instances on a large-scale, multi-core compute cluster. We analyze the impact of the distributed algorithms employed, the problem instance characteristics and network overhead. Finally, we show that the model checker can even obtain good performance in a high-bandwidth computational grid environment. Model checking is a popular technique to systematically and automatically verify system properties. Unfortunately, the well-known state explosion problem often limits the extent to which it can be applied to realistic specifications, due to the huge resulting memory requirements. Distributed-memory model checkers exist, but have thus far only been evaluated on small-scale clusters, with mixed results. We examine one well-known distributed model checker, DiVinE, in detail, and show how a number of additional optimizations in its runtime system enable it to efficiently check very demanding problem instances on a large-scale, multi-core compute cluster. We analyze the impact of the distributed algorithms employed, the problem instance characteristics and network overhead. Finally, we show that the model checker can even obtain good performance in a high-bandwidth computational grid environment. (en)
Title	Efficient Large-Scale Model Checking Efficient Large-Scale Model Checking (en)
skos:prefLabel	Efficient Large-Scale Model Checking Efficient Large-Scale Model Checking (en)
skos:notation	RIV/00216224:14330/09:00029324!RIV11-GA0-14330___
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(GA201/09/1389), P(GP201/09/P497), Z(MSM0021622419)
http://linked.open...vai/riv/dodaniDat	2011
http://linked.open...aciTvurceVysledku	Barnat, Jiří Brim, Luboš
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Masarykova univerzita / Fakulta informatiky
http://linked.open...dnocenehoVysledku	312510
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/09:00029324
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	model checking; distributed; parallel; large-scale (en)
http://linked.open.../riv/klicoveSlovo	model checking distributed large-scale parallel
http://linked.open...ontrolniKodProRIV	[C194C75B5C32]
http://linked.open...v/mistoKonaniAkce	Rome, Italy
http://linked.open...i/riv/mistoVydani	IEEE
http://linked.open...i/riv/nazevZdroje	23rd IEEE International Parallel & Distributed Processing Symposium
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	2 (xsd:int)
http://linked.open...cetTvurcuVysledku	4 (xsd:int)
http://linked.open...vavai/riv/projekt	Verification and Analysis of Large-Scale Computer Systems Automated formal verification using modern hardware
http://linked.open...UplatneniVysledku	2009
http://linked.open...iv/tvurceVysledku	Barnat, Jiří Brim, Luboš Bal, Henri E. Verstoep, Kees
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open...ain/vavai/riv/wos	000272993600019
http://linked.open.../riv/zahajeniAkce	2009-01-01 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	1530-2075
number of pages	12 (xsd:int)
http://purl.org/ne...btex#hasPublisher	IEEE
https://schema.org/isbn	978-1-4244-3751-1
http://localhost/t...ganizacniJednotka	14330
is http://linked.open...avai/riv/vysledek of	Efficient Large-Scale Model Checking Efficient Large-Scale Model Checking Efficient Large-Scale Model Checking

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software