|Algorithmic Verification Boundaries for Infinite-State Systems|
|Funding: Grant Agency of Czech Republic, Project No. 201/97/0456|
|Starting Date: January 1, 1997|
|Duration: 3 years|
|Coordinator: P. Jancar (TU Ostrava)|
|Project Leader at FI: M. Kretinsky|
|Description||The project is motivated by a live current research area concerning
analysis and verification of complex (infinite-state) concurrent
systems. It is the area of boundaries for algorithmic verification,
where verification means checking equivalences of systems, their
temporal logic properties etc.
Recently, several interesting results have been obtained in the given area, e.g. for calculi BPA, BPP, and Petri nets, to which also the grant of the Grant Agency of the Czech Republic, grant no. 201/93/2123 by the same research team, has contributed.
The main target of the proposed project is to explore systematically the mentioned and related models and focus on
Faculty of Informatics, Masaryk
Technical University Ostrava
L. Brim (FI)
I. Cerna (FI)
P. Jancar (TU Ostrava)
M. Kretinsky (FI)
A. Kucera (FI)
J. Srba (FI)
|Publications||List of publications (by FI staff only)|
The workshop was organised as a part of the project with focus on the problem of modelling, testing, and verification of concurrent systems. This area has recently attracted a lot of attention - a large theory answering many interesting questions has been developed, and parts of the theory have also been applied. The aim of the workshop was to highlight promising theoretical approaches and paradigms which affect the development of practical tools for (semi)automatic verification of concurrent systems. Working experimental tools were presented.