• česky
  • english
Přejít na obsah | Přejít na menu

Informační systém výzkumu, experimentálního vývoje a inovací
výzkum, vývoj a inovace podporované z veřejných prostředků ČR

    • Poskytovatelé podpory ve výzkumu, vývoji a inovacích (RPO)
    • Programy výzkumu, vývoje a inovací (RPG)
    • Subjekty ve výzkumu, vývoji a inovacích (RPR)
  • Veřejné soutěže ve výzkumu, vývoji a inovacích (VES)
  • Projekty výzkumu, vývoje a inovací (CEP)
  • Výzkumné záměry (CEZ)
  • Výsledky výzkumu, vývoje a inovací (RIV)

GA201/06/1338 - Automatizovaná verifikace softwaru (2006-2008, GA0/GA)

Údaje o projektu
Identifikační kódGA201/06/1338
Důvěrnost údajůS - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
Název v původním jazyceAutomatizovaná verifikace softwaru
PoskytovatelGA0 - Grantová agentura České republiky (GA ČR)
ProgramGA - Standardní projekty (1993-…)
Kategorie VaVZV - Základní výzkum
Hlavní oborIN - Informatika
Zahájení řešení1.1.2006
Ukončení řešení31.12.2008
Datum posledního uvolnění účelové podpory25.4.2008
Číslo smlouvy201/06/1338
Poslední stav řešeníU - Ukončený projekt, tj. jednoletý nebo víceletý projekt, který skončil v předcházejícím roce, v příslušném roce sběru dat jsou dodány údaje vztahující se k jeho ukončení
Finance projektu
Období200620072008celkem
Výše podpory ze státního rozpočtu458 tis. Kč480 tis. Kč492 tis. Kč1 430 tis. Kč
Celkové uznané náklady458 tis. Kč480 tis. Kč492 tis. Kč1 430 tis. Kč
Typskutečně čerpanéskutečně čerpanéskutečně čerpané
Druh soutěžeVS - Veřejná soutěž ve výzkumu a vývoji
Veřejná soutěž ve výzkumu, vývoji a inovacíchSGA02006GA-ST - Veřejná soutěž (GA0/GA)
Cíle řešení v původním jazyceHlavním cílem projektu je vytvoření teoreticko-metodologického zázemí počítačem podporované a automatické verifikace softwarových systémů. Projekt si klade za úkol podpořit vývoj metodologií, technologií a nástrojů softwarového inženýrství v oblasti technik automatické verifikace. Projekt přispěje k výzkumu směřujícímu k rozvoji poznatků o technologiích pro realistické modelování softwarových systémů, včetně systémů reálného času, specielně s ohledem na bezpečnost jejich provozu. Cílem je navrhnout efektivní implementace těchto modelů a na nich založených metodologiích pro efektivní verifikaci. Projekt se zaměří na zapouzdřené, distribuované a paralelní systémy. Vzhledem k výpočetní náročnosti a rozsáhlosti procesu verifikace je cílem navrhnout metodologie využívající v maximální míře i nové možnosti výpočetních technologií, např. ve smyslu paralelního a distribuovaného počítaní a v hierarchickém přístupu k paměti.
Klíčová slova v anglickém jazyceverification; model-checking; software; components
Hodnocení výsledkůV - Vynikající výsledky (s mezinárodním významem apod.). Zároveň byly splněny cíle a předpokládané výsledky uvedené ve smlouvě / rozhodnutí o poskytnutí podpory.
Zhodnocení výsledků řešení českyHlavní výsledky projektu jsou nové původní metody a techniky pro automatizovanou verifikaci velkých softwarových systémů, s důrazem na praktičnost jejich aplikace na realistické systémy, jejich optimalizace a vytvoření softwarové podpory pro jejich použí
Rok dodání údajů do CEP2009
Systémové označení dodávky datCEP09-GA0-GA-U/02:2
Datum dodání záznamu22.10.2009
Účastníci projektu
Počet příjemců1
Počet dalších účastníků projektu0
Příjemce / Organizační jednotka garantující řešeníMasarykova univerzita / Fakulta informatiky
ŘešitelProf. RNDr. Luboš Brim, CSc. (státní příslušnost: CZ - Česká republika; tel.: 549 493 647; fax: 549 491 820)
Finance účastníků projektu
Poznámka: Finance účastníků projektu jsou sledovány od roku 2007
Výše podpory ze státního rozpočtu
Účastník20072008
Masarykova univerzita / Fakulta informatiky480 tis. Kč492 tis. Kč
Celkové uznané náklady
Účastník20072008
Masarykova univerzita / Fakulta informatiky480 tis. Kč492 tis. Kč
Výsledky projektu v RIV
Počet výsledků v RIV45
Výsledek druhu JRIV/00216224:14330/11:00049402 - Flash memory efficient LTL model checking (2011)
Výsledek druhu DRIV/00216224:14330/09:00028658 - Can Flash Memory Help in Model Checking? (2009)
Výsledek druhu JRIV/00216224:14330/09:00029078 - On Decidability of LTL Model Checking for Process Rewrite Systems (2009)
Výsledek druhu CRIV/00216224:14330/08:00024133 - Component-Interaction Automata Approach (CoIn) (2008)
Výsledek druhu RRIV/00216224:14330/08:00024473 - DiVinE Cluster (2008)
Výsledek druhu DRIV/00216224:14330/08:00024321 - DiVinE Multi-Core -- A Parallel LTL Model-Checker (2008)
Výsledek druhu ORIV/00216224:14330/08:00024337 - Estimating State Space Parameters (2008)
Výsledek druhu JRIV/00216224:14330/08:00024165 - Improved Distributed Algorithms for SCC Decomposition (2008)
Výsledek druhu DRIV/00216224:14330/09:00028657 - Local Quantitative LTL Model Checking (2009)
Výsledek druhu JRIV/00216224:14330/08:00024164 - Petri Nets Are Less Expressive Than State-Extended PA (2008)
Výsledek druhu RRIV/00216224:14330/08:00024418 - ProbDiVinE-MC (2008)
Výsledek druhu DRIV/00216224:14330/08:00024323 - ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems (2008)
Výsledek druhu DRIV/00216224:14330/08:00024177 - Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking (2008)
Výsledek druhu DRIV/00216224:14330/08:00024282 - Semi-external LTL Model Checking (2008)
Výsledek druhu JRIV/00216224:14330/08:00024166 - Shared Hash Tables in Parallel Model Checking (2008)
Výsledek druhu DRIV/00216224:14330/08:00024322 - Squeeze All the Power Out of Your Hardware to Verify Your Software! (2008)
Výsledek druhu JRIV/00216224:14330/07:00019439 - Component Substitutability via Equivalencies of Component-Interaction Automata (2007)
Výsledek druhu RRIV/00216224:14330/07:00019614 - DiVinE Multi-Core (2007)
Výsledek druhu JRIV/00216224:14330/07:00019458 - Improved Distributed Algorithms for SCC Decomposition (2007)
Výsledek druhu DRIV/00216224:14330/07:00019426 - I/O Efficient Accepting Cycle Detection (2007)
Výsledek druhu DRIV/00216224:14330/07:00019356 - Model Checking Large Finite-State Systems and Beyond (2007)
Výsledek druhu DRIV/00216224:14330/07:00019374 - Parallel Algorithms for Finding SCCs in Implicitly Given Graphs (2007)
Výsledek druhu JRIV/00216224:14330/07:00019374 - Parallel Algorithms for Finding SCCs in Implicitly Given Graphs (2007)
Výsledek druhu DRIV/00216224:14330/07:00019460 - Parallel Model Checking and the FMICS-jETI Platform (2007)
Výsledek druhu RRIV/00216224:14330/07:00024472 - ProbDiVinE (2007)
Výsledek druhu DRIV/00216224:14330/07:00019497 - Relaxed Cycle Condition Improves Partial Order Reduction (2007)
Výsledek druhu DRIV/00216224:14330/07:00019427 - Scalable Multi-core LTL Model-Checking (2007)
Výsledek druhu JRIV/00216224:14330/07:00019427 - Scalable Multi-core LTL Model-Checking (2007)
Výsledek druhu JRIV/00216224:14330/07:00019459 - Shared Hash Tables in Parallel Model Checking (2007)
Výsledek druhu DRIV/00216224:14330/07:00020381 - Tutorial: Parallel Model Checking (2007)
Výsledek druhu JRIV/00216224:14330/07:00020381 - Tutorial: Parallel Model Checking (2007)
Výsledek druhu DRIV/00216224:14330/07:00019329 - Verifying VHDL Designs with Multiple Clocks in SMV (2007)
Výsledek druhu DRIV/00216224:14330/06:00015451 - Cluster-Based LTL Model Checking of Large Systems (2006)
Výsledek druhu JRIV/00216224:14330/06:00015451 - Cluster-Based LTL Model Checking of Large Systems (2006)
Výsledek druhu DRIV/00216224:14330/06:00015414 - Component Substitutability via Equivalencies of Component-Interaction Automata (2006)
Výsledek druhu JRIV/00216224:14330/06:00015452 - Distributed breadth-first search LTL model checking (2006)
Výsledek druhu DRIV/00216224:14330/06:00015450 - Distributed Qualitative LTL Model Checking of Markov Decision Processes (2006)
Výsledek druhu DRIV/00216224:14330/06:00015443 - DiVinE -- A Tool for Distributed Verification (2006)
Výsledek druhu JRIV/00216224:14330/06:00015443 - DiVinE -- A Tool for Distributed Verification (2006)
Výsledek druhu RRIV/00216224:14330/06:00024474 - DiVinE Library (2006)
Výsledek druhu JRIV/00216224:14330/06:00015466 - Model Checking of RegCTL (2006)
Výsledek druhu DRIV/00216224:14330/06:00015442 - On Combining Partial Order Reduction with Fairness Assumptions (2006)
Výsledek druhu DRIV/00216224:14330/06:00015417 - On Decidability of LTL Model Checking for Process Rewrite Systems (2006)
Výsledek druhu JRIV/00216224:14330/06:00015417 - On Decidability of LTL Model Checking for Process Rewrite Systems (2006)
Výsledek druhu ARIV/00216224:14330/06:00015439 - On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems (2006)
Tuto aplikaci pro Radu pro výzkum, vývoj a inovace provozuje Výpočetní a informační centrum Českého vysokého učení technického v Praze. Vyvíjí InfoScience Praha s.r.o.. Verze aplikace 1.6.15. Datové schéma ISVAV_WEB5_00318. Podpora uživatelů na e-mailové adrese podpora (zavináč) isvav (tečka) cz nebo telefonním čísle 224 234 797 (v pracovních dnech 8-16 hod.).