• č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)

RIV/00216305:26230/08:PR23748 - Model checking Using Symbolic Execution (2008)

Údaje o výsledku
Identifikační kódRIV/00216305:26230/08:PR23748
Název v původním jazyceModel checking Using Symbolic Execution
DruhR - Software
Jazykeng - angličtina
OborJC - Počítačový hardware a software
Rok uplatnění2008
Kód důvěrnosti údajůS - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
Počet výskytů výsledku4
Tvůrci výsledku
Počet tvůrců celkem4
Počet domácích tvůrců1
TvůrceKřena Bohuslav (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; G - garant výsledku)
TvůrceBraione Pietro (státní příslušnost: IT - Italská republika)
TvůrceDenaro Giovanni (státní příslušnost: IT - Italská republika)
TvůrcePezze Mauro (státní příslušnost: IT - Italská republika)
Údaje blíže specifikující výsledek
Popis v původním jazyceMUSE is a prototype implementation of a tool for verification of LTL properties against Java byte-code which uses symbolic execution technique for combatting the state space explosion problem.
Klíčová slovaSymbolic execution, code-based model checking of software.
Interní identifikační kód produktu přidělený tvůrcemMUSE
Lokalizacehttp://www.fit.vutbr.cz/research/groups/verifit/tools/muse/
Technické parametryNástroj pro svůj běh vyžaduje následující nástroje: 1. Java SE Development Kit 6, 2. Eclipse, 3. GNU C/C++ překladač g++ a make, 4. SICStus Prolog nebo CVC3, 5. Spin nebo LTL2BA.
IČ vlastníka výsledku00216305
Název vlastníkaVysoké učení technické v Brně
Stát vlastníkaCZ - Česká republika
Druh možnosti využitíN - Nabytí licence není nutné (výsledek není licencován)
Údaje o tomto záznamu o výsledku
PředkladatelVysoké učení technické v Brně / Fakulta informačních technologií
DodavatelGA0 - Grantová agentura České republiky (GA ČR)
Rok sběru2010
Systémové označení dodávky datRIV10-GA0-26230___/02:2
Datum dodání25.5.2010
SpecifikaceRIV/00216305:26230/08:PR23748!RIV10-GA0-26230___
Kontrolní kód[07129D67EC5D]
Další výskyty tohoto výsledku od stejného předkladatele
Dodáno GA ČR v roce 2009Záznam s identifikačním kódem RIV/00216305:26230/08:PR23748 v dodávce dat RIV09-GA0-26230___/02:2
Dodáno MŠMT v roce 2009Záznam s identifikačním kódem RIV/00216305:26230/08:PR23748 v dodávce dat RIV09-MSM-26230___/03:3
Dodáno MŠMT v roce 2010Záznam s identifikačním kódem RIV/00216305:26230/08:PR23748 v dodávce dat RIV10-MSM-26230___/01:1
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
ProjektGA102/07/0322 - Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů (2007-2009, GA0/GA)
ProjektGP102/06/P076 - Metody a nástroje pro automatizované odhalování softwarových chyb (2006-2008, GA0/GP)
Výzkumný záměrMSM0021630528 - Výzkum informačních technologií z hlediska bezpečnosti (2007-2013, MSM)
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_00304. 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.).