About: Tree Automata In Modelling And Verification Of Concurrent Programs

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

About: Tree Automata In Modelling And Verification Of Concurrent Programs 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 consider the problem of automated formal verification of modern concurrent software systems. Dealing with such systems, which involves handling unbounded dynamic instantiation, recursion, etc., naturally leads to a need of dealing with infinite state spaces. We suppose states of such systems to be viewed as terms with a tree structure and in the future, we would like to use the regular tree model checking method for dealing with infinite sets of states. Infinite sets of states are to be finitely described by tree automata and their transformations by tree transducers. To facilitate the termination of the method, we intend to use a generalization of the abstract regular model checking method proposed for linear words. In the paper, we discuss the starting points of our work, the problems to be solved, and briefly sketch our first preliminary steps in the area---namely steps leading to a library for handling tree automata and transducers to be used as a basis for our future verification tool. We consider the problem of automated formal verification of modern concurrent software systems. Dealing with such systems, which involves handling unbounded dynamic instantiation, recursion, etc., naturally leads to a need of dealing with infinite state spaces. We suppose states of such systems to be viewed as terms with a tree structure and in the future, we would like to use the regular tree model checking method for dealing with infinite sets of states. Infinite sets of states are to be finitely described by tree automata and their transformations by tree transducers. To facilitate the termination of the method, we intend to use a generalization of the abstract regular model checking method proposed for linear words. In the paper, we discuss the starting points of our work, the problems to be solved, and briefly sketch our first preliminary steps in the area---namely steps leading to a library for handling tree automata and transducers to be used as a basis for our future verification tool. (en)
Title	Tree Automata In Modelling And Verification Of Concurrent Programs Tree Automata In Modelling And Verification Of Concurrent Programs (en)
skos:prefLabel	Tree Automata In Modelling And Verification Of Concurrent Programs Tree Automata In Modelling And Verification Of Concurrent Programs (en)
skos:notation	RIV/00216305:26230/04:PU49269!RIV11-MSM-26230___
http://linked.open...avai/riv/aktivita	N P V Z
http://linked.open...avai/riv/aktivity	N, P(GA102/04/0780), P(GP102/03/D211), V, Z(MSM 262200012)
http://linked.open...vai/riv/dodaniDat	2011
http://linked.open...aciTvurceVysledku	Vojnar, Tomáš Rogalewicz, Adam
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	Vysoké učení technické v Brně / Fakulta informačních technologií
http://linked.open...dnocenehoVysledku	590757
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/04:PU49269
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	formal verification, regular model checking, automated abstraction (en)
http://linked.open.../riv/klicoveSlovo	regular model checking formal verification automated abstraction
http://linked.open...ontrolniKodProRIV	[7916D955E066]
http://linked.open...v/mistoKonaniAkce	Sv. Hostýn
http://linked.open...i/riv/mistoVydani	Ostrava
http://linked.open...i/riv/nazevZdroje	Proceedings of ASIS 2004
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	2 (xsd:int)
http://linked.open...cetTvurcuVysledku	2 (xsd:int)
http://linked.open...vavai/riv/projekt	Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems Automated methods and tools supporting development of reliable concurrent and distributed systems
http://linked.open...UplatneniVysledku	2004
http://linked.open...iv/tvurceVysledku	Vojnar, Tomáš Rogalewicz, Adam
http://linked.open...vavai/riv/typAkce	EUR - Evropská
http://linked.open.../riv/zahajeniAkce	2004-09-22 (xsd:date)
http://linked.open...n/vavai/riv/zamer	http://linked.opendata.cz/resource/domain/vavai/zamer/MSM%20262200012
number of pages	6 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Neuveden
https://schema.org/isbn	80-86840-03-4
http://localhost/t...ganizacniJednotka	26230

Faceted Search & Find service v1.16.116 as of Feb 22 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

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