Project information
Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II.
(FI MAV II.)
- Project Identification
- MUNI/A/0760/2012
- Project Period
- 1/2013 - 12/2013
- Investor / Pogramme / Project type
-
Masaryk University
- Grant Agency of Masaryk University
- Category A
- MU Faculty or unit
-
Faculty of Informatics
- prof. RNDr. Mojmír Křetínský, CSc.
- RNDr. Tomáš Babiak, Ph.D.
- prof. RNDr. Jiří Barnat, Ph.D.
- prof. RNDr. Luboš Brim, CSc.
- prof. RNDr. Ivana Černá, CSc.
- Mgr. Sven Dražan
- prof. RNDr. Jozef Gruska, DrSc.
- prof. RNDr. Petr Hliněný, Ph.D.
- Mgr. Petr Jarušek, Ph.D.
- RNDr. Pavel Karas, Ph.D.
- prof. RNDr. Michal Kozubek, Ph.D.
- RNDr. Jan Krčál, Ph.D.
- prof. Dr. rer. nat. RNDr. Mgr. Bc. Jan Křetínský, Ph.D.
- prof. RNDr. Antonín Kučera, Ph.D.
- RNDr. Jiří Matela, Ph.D.
- prof. RNDr. Luděk Matyska, CSc.
- RNDr. Ondrej Moriš
- doc. RNDr. Petr Novotný, Ph.D.
- doc. Mgr. Radek Pelánek, Ph.D.
- RNDr. Petr Ročkai, Ph.D.
- doc. Mgr. Hana Rudová, Ph.D.
- RNDr. David Sehnal, Ph.D.
- RNDr. Mária Svoreňová, Ph.D.
- Mgr. Karel Štěpka, Ph.D.
- Mgr. Marek Trtík, Ph.D.
- RNDr. Jana Tůmová, Ph.D.
Projekt je zaměřen na podporu výzkumné a vývojové činnosti studentů doktorského a magisterského studia, kteří jsou vedeni převážně školiteli, kteří participovali na stejnojmenném projektu specifického výzkumu z let 2010-12 řešeném na FI MU a na Výzkumném záměru Fakulty informatiky MU „Vysoce paralelní a distribuované výpočetní systémy“ řešeném v letech 2005-2011.
Problematika navrhovaného projektu na uvedené projekty navazuje a dále ji rozšiřuje o perspektivní a originální směry výzkumu tak, aby došlo k dalšímu rozvoji doktorského studia vzhledem k synergii s projekty operační programů VaVpI a Podnikání a inovace, zejména v návaznosti na využití výzkumu směrem k aplikacím a budovanému centru CERIT.
Jedná se o výzkum a vývoj v oblastech použití formálních metod při modelování, analýze a verifikaci: klasických a zejména stochastických systémů i nekonečně stavových, komplexních a softwarově intenzivních systémů, vestavných systémů, komunikačních protokolů a dalších, zejména biologických systémů a kvantových výpočtů a analýzu jejich vlastností. Další oblastí je analýza medicínského obrazu, včetně nově vyvíjených metod analýzy s pomocí HW a/nebo SW prostředků.
Tyto oblasti jsou na aplikační úrovni často provázány na využívání rozsáhlých výpočetních systémů a moderních paralelních architektur, např. typu CUDA, GPGPU (General Purpose Graphic Processing Unit) a many-core GPU.
Další popis projektu je strukturován dle oblastí, jež jsou vedeny jednotlivými školiteli pod následujícími zkratkami:
A: doc. RNDr. Jiří Barnat, PhD.;
B: prof. RNDr. Luboš Brim, CSc.;
C: prof. RNDr. Ivana Černá, CSc.;
D: prof. RNDr. Jozef Gruska, DrSc;.
E: doc. RNDr. Petr Hliněný, Ph.D.;
F: prof. RNDr. Michal Kozubek, PhD.;
G: prof. RNDr. Mojmír Křetínský, CSc.;
H: prof. RNDr. Antonín Kučera, PhD.;
I: prof. RNDr. Luděk Matyska, CSc.;
J: doc. Mgr. Radek Pelánek, PhD.;
K: doc. Mgr. Hana Rudová, Ph.D.
Oblasti jsou po obsahové stránce specifikovány níže v části "Odborná charakteristika projektu".
Publications
Total number of publications: 43
2014
-
Model Checking Parallel Programs with Inputs
Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP), year: 2014
-
Temporal Verification of Simulink Diagrams
Proceedings of HASE 2014, year: 2014
2013
-
Algorithms for Efficient Computation of Convolution
Design and Architectures for Digital Signal Processing, edition: Vyd. 1st ed., year: 2013, number of pages: 30 s.
-
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
Computer Aided Verification - 25th International Conference, CAV 2013, year: 2013
-
Automatic Detection of Concepts from Problem Solving Times
Artificial Intelligence in Education, year: 2013
-
ClabureDB: Classified Bug-Reports Database Tool for Developers of Program Analysis Tools
Verification, Model Checking, and Abstract Interpretation: 14th International Conference, VMCAI 2013, year: 2013
-
Compact Symbolic Execution
11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, year: 2013
-
Comparison of LTL to Deterministic Rabin Automata Translators
Logic for Programming Artificial Intelligence and Reasoning, LPAR-19, year: 2013
-
Compositional Approach to Suspension and Other Improvements to LTL Translation
Model Checking Software - 20th International Symposium, SPIN 2013, year: 2013
-
Compositional Verification and Optimization of Interactive Markov Chains
CONCUR 2013 - Concurrency Theory - 24th International Conference, year: 2013