Attributes | Values |
---|
rdf:type
| |
rdfs:seeAlso
| |
Description
| - The project contributes to the research planned within the COST action IC0901: Rich Model Toolkit – An Infrastructure for Reliable Computer Systems, which is targeted at (1) development of a language for describing in a homogeneous way a broad range of computer systems to be verified and (2) research in the area of methods for formal verification with the goal of significantly increasing their generality, efficiency, and degree of automation. The proposed project in particular considers two aspects of the systems dealt with in the COST action IC0901 that constitute a very significant challenge for the current verification methods. Namely, the project considers development of new verification methods for computer systems with complex data structures (including dynamic data structures based on pointers) and/or with advanced features of concurrency. In the former case, the project concentrates on research on symbolic verification methods based on the theory of automata, logics, and their combinations. (en)
- Cílem projektu je přispět výzkumem realizovaným v koordinaci s COST akcí IC0901 k výraznému zlepšení obecnosti a efektivnosti metod automatické verifikace počítačových systémů se složitými datovými strukturami a pokročilými rysy paralelismu.
|
Title
| - Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit (en)
- Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit
|
skos:notation
| |
http://linked.open...avai/cep/aktivita
| |
http://linked.open...kovaStatniPodpora
| |
http://linked.open...ep/celkoveNaklady
| |
http://linked.open...datumDodatniDoRIV
| |
http://linked.open...i/cep/druhSouteze
| |
http://linked.open...ep/duvernostUdaju
| |
http://linked.open.../cep/fazeProjektu
| |
http://linked.open...ai/cep/hlavniObor
| |
http://linked.open...hodnoceniProjektu
| |
http://linked.open...vai/cep/kategorie
| |
http://linked.open.../cep/klicovaSlova
| - Automated verification; programs with complex data structures; concurrent systems; symbolic verification; static and dynamic analysis; model checking; theory of automata and logics (en)
|
http://linked.open...ep/partnetrHlavni
| |
http://linked.open...inujicichPrijemcu
| |
http://linked.open...cep/pocetPrijemcu
| |
http://linked.open...ocetSpoluPrijemcu
| |
http://linked.open.../pocetVysledkuRIV
| |
http://linked.open...enychVysledkuVRIV
| |
http://linked.open...lneniVMinulemRoce
| |
http://linked.open.../prideleniPodpory
| |
http://linked.open...iciPoslednihoRoku
| |
http://linked.open...atUdajeProjZameru
| |
http://linked.open.../vavai/cep/soutez
| |
http://linked.open...usZobrazovaneFaze
| |
http://linked.open...ai/cep/typPojektu
| |
http://linked.open...ep/ukonceniReseni
| |
http://linked.open.../cep/vedlejsiObor
| |
http://linked.open...ep/zahajeniReseni
| |
http://linked.open...jektu+dodavatelem
| - Tree automata inclusion testing was optimized, automation of forest-automata-based verification of programs with pointers was increased, and a new graph-based method for verifying memory operations of a very low level was proposed. Noise-based testing of concurrent programs was extended by using the genetic algorithm for setting noise parameters and extended to C/C++ programs on the binary level. (en)
- Bylo zefektivněno testování inkluze nad stromovými automaty, zvýšena automatizace verifikace programů s ukazateli pomocí automatů nad lesy a navržen nový grafový přístup pro verifikaci paměťových operací velmi nízké úrovně. Testování paralelních programů pomocí vkládání šumu bylo doplněno o užití genetického algoritmu pro nastavení parametrů šumu a rozšířeno i na C/C++ programy na binární úrovni. (cs)
|
http://linked.open...tniCyklusProjektu
| |
http://linked.open.../cep/klicoveSlovo
| - model checking
- symbolic verification
- concurrent systems
- programs with complex data structures
- static and dynamic analysis
- Automated verification
|
is http://linked.open...vavai/riv/projekt
of | |
is http://linked.open...vavai/cep/projekt
of | |