About: Concrete Search with Abstract Matching and Refinement

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

About: Concrete Search with Abstract Matching and Refinement 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	We propose an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. The method does not require an abstract transition relation to be generated, but instead executes the concrete transitions while storing abstract versions of the concrete states, as specified by a set of abstraction predicates. For each explored transition the method checks, with the help of a theorem prover, whether there is any loss of precision introduced by abstraction. The results of these checks are used to decide termination or to refine the abstraction by generating new abstraction predicates. If the (possibly infinite) concrete system under analysis has a finite bisimulation quotient, then the method is guaranteed to eventually explore an equivalent finite bisimilar structure. We propose an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. The method does not require an abstract transition relation to be generated, but instead executes the concrete transitions while storing abstract versions of the concrete states, as specified by a set of abstraction predicates. For each explored transition the method checks, with the help of a theorem prover, whether there is any loss of precision introduced by abstraction. The results of these checks are used to decide termination or to refine the abstraction by generating new abstraction predicates. If the (possibly infinite) concrete system under analysis has a finite bisimulation quotient, then the method is guaranteed to eventually explore an equivalent finite bisimilar structure. (en)
Title	Concrete Search with Abstract Matching and Refinement Concrete Search with Abstract Matching and Refinement (en)
skos:prefLabel	Concrete Search with Abstract Matching and Refinement Concrete Search with Abstract Matching and Refinement (en)
skos:notation	RIV/00216224:14330/05:00012728!RIV10-GA0-14330___
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(1ET408050503), P(1M0545), P(GA201/03/0509), P(GD102/05/H050), Z(MSM0021622419)
http://linked.open...vai/riv/dodaniDat	2010
http://linked.open...aciTvurceVysledku	Pelánek, Radek
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	516164
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/05:00012728
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	model checking; predicate abstraction; under-approximation (en)
http://linked.open.../riv/klicoveSlovo	predicate abstraction model checking under-approximation
http://linked.open...ontrolniKodProRIV	[8A1882FADC82]
http://linked.open...v/mistoKonaniAkce	Edinburgh
http://linked.open...i/riv/mistoVydani	Edinburgh
http://linked.open...i/riv/nazevZdroje	Computer Aided Verification
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	Institute for Theoretical Computer Science Integrated Approach to Education of PhD Students in the Area of Parallel and Distributed Systems Automated Verification of Parallel and Distributed Systems Techniques for automatic verification and validation of software and hardware systems
http://linked.open...UplatneniVysledku	2005
http://linked.open...iv/tvurceVysledku	Pelánek, Radek Pasareanu, Corina Visser, Willem
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2005-01-01 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
number of pages	15 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	3-540-27231-3
http://localhost/t...ganizacniJednotka	14330
is http://linked.open...avai/riv/vysledek of	Concrete Search with Abstract Matching and Refinement

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