Cut-offs and Automata in Formal Verification of Infinite-State Systems
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F07%3APU70808" target="_blank" >RIV/00216305:26230/07:PU70808 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Cut-offs and Automata in Formal Verification of Infinite-State Systems
Original language description
In this work, we discuss two complementary approaches to formal verification of infinite-state systems---namely, the use cut-offs and automata-based symbolic model checking (especially the so-called regular model checking). The thesis is based on extended versions of multiple conference and journal papers joint into a unified framework and accompanied with a significantly extended overview of other existing approaches.<br> <br> The presented original results include cut-offs for verification of parameterised networks of processes with shared resources, the approach of abstract regular model checking combining regular model checking with the counterexample-guided abstraction refinement (CEGAR) loop, a proposal of using language inference for regular model checking, techniques for an application of regular model checking to verification of programs manipulating dynamic linked data structures, the approach of abstract regular tree model checking as well as a proposal of a novel class of t
Czech name
Řezy a automaty ve formální verifikaci nekonečně stavových systémů
Czech description
Tato práce diskutuje využití řezů a automatů ve formální verifikaci nekonečně stavových systémů.
Classification
Type
B - Specialist book
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
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)<br>Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2007
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
ISBN
978-80-214-3547-6
Number of pages
189
Publisher name
Faculty of Information Technology BUT
Place of publication
Brno
UT code for WoS book
—