About: Scalable shared memory LTL model checking

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

About: Scalable shared memory LTL 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	Recent development in computer hardware has brought more wide-spread emergence of shared memory, multi-core systems. These architectures offer opportunities to speed up various tasks - model checking and reachability analysis among others. In this paper, we present a design for a parallel shared memory LTL model checker that is based on a distributed memory algorithm. To improve the scalability of our tool, we have devised a number of implementation techniques which we present in this paper. We also report on a number of experi- ments we conoducted to analyze the behaviour of our tool under different conditions using various models. We demonstrate that our tool exhibits significant speedup in comparison to sequential tools, which improves the workflow of verification in general. Recent development in computer hardware has brought more wide-spread emergence of shared memory, multi-core systems. These architectures offer opportunities to speed up various tasks - model checking and reachability analysis among others. In this paper, we present a design for a parallel shared memory LTL model checker that is based on a distributed memory algorithm. To improve the scalability of our tool, we have devised a number of implementation techniques which we present in this paper. We also report on a number of experi- ments we conoducted to analyze the behaviour of our tool under different conditions using various models. We demonstrate that our tool exhibits significant speedup in comparison to sequential tools, which improves the workflow of verification in general. (en)
Title	Scalable shared memory LTL model checking Scalable shared memory LTL model checking (en)
skos:prefLabel	Scalable shared memory LTL model checking Scalable shared memory LTL model checking (en)
skos:notation	RIV/00216224:14330/10:00065778!RIV14-MSM-14330___
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(1ET408050503), P(1M0545), P(GA201/09/1389), P(GP201/09/P497), S, Z(MSM0021622419)
http://linked.open...iv/cisloPeriodika	2
http://linked.open...vai/riv/dodaniDat	2014
http://linked.open...aciTvurceVysledku	Barnat, Jiří Brim, Luboš Ročkai, Petr
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
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	286416
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/10:00065778
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	LTL Model Cecking; Parallel; Shared-Memory (en)
http://linked.open.../riv/klicoveSlovo	Parallel LTL Model Cecking Shared-Memory
http://linked.open...odStatuVydavatele	DE - Spolková republika Německo
http://linked.open...ontrolniKodProRIV	[23E2D26EBBE6]
http://linked.open...i/riv/nazevZdroje	International Journal on Software Tools for Technology Transfer (STTT)
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	3 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	Institute for Theoretical Computer Science Verification and Analysis of Large-Scale Computer Systems Automated formal verification using modern hardware Techniques for automatic verification and validation of software and hardware systems
http://linked.open...UplatneniVysledku	2010
http://linked.open...v/svazekPeriodika	12
http://linked.open...iv/tvurceVysledku	Barnat, Jiří Brim, Luboš Ročkai, Petr
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	1433-2779
number of pages	15 (xsd:int)
http://bibframe.org/vocab/doi	10.1007/s10009-010-0136-z
http://localhost/t...ganizacniJednotka	14330

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, 44 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software