Abstract Regular Model Checking

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F04%3APU49082" target="_blank" >RIV/00216305:26230/04:PU49082 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Abstract Regular Model Checking
Original language description
We propose abstract regular model checking as a new generic technique for verification of parametric and infinite-state systems. The technique combines the two approaches of regular model checking and verification by abstraction. We propose a general framework of the method as well as several concrete ways of abstracting automata or transducers, which we use for modelling systems and encoding sets of their configurations as usual in regular model checking. The abstraction is based on collapsing states oof automata (or transducers) and its precision is being incrementally adjusted by analysing spurious counterexamples. We illustrate the technique on verification of a wide range of systems including a novel application of automata-based techniques to anexample of systems with dynamic linked data structures.
Czech name
Abstraktní regulární model checking
Czech description
V článku je navržen koncept originální metody symbolické verifikace využívající abstrakce nad konečnými automaty popisujícími (případně nekonečné) množiny stavů zkoumaných systémů. Abstrakce se zde projevuje slučováním stavů automatů, jež mají určitým způsobem podobné vlastnosti. Využití postupně zjemňované abstrakce zajišťuje konečnost a vysokou efektivitu výpočtu množiny dosažitelných stavů v řadě praktických případů.<br>

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
JC - Computer hardware and software
OECD FORD branch
—

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2004
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)