Red Hat collaborates with the universities not only on development and student activities, but also on applied research. Wide portfolio of software products provides many opportunities for application of the state-of-the-art methods and techniques, especially in fields like software engineering, software quality or security.
Red Hat offers the researchers opportunities for performing industrial case studies, provides real-world data for experiments and supports junior researchers by providing them connections to industry experts. Red Hat employees are also closely collaborating with university research groups, directly contributing to research efforts.
Red Hat laboratories
Students have the opportunity to join established research groups within the university and focus on deeper issues that impact the open-source community.
Lab Q at Faculty of Information Technology, Brno University of Technology (FIT BUT)
Faculty of informatics, Masaryk University (FI MU) open-source lab
Currently, Czech dictionaries for machine usage are either small or proprietary. Daniela Ryšavá (FI MU) is discovering methods that lead to automatic extraction of related words. At the end of the project, dictionary with 100.000 entries will be available for full text search, data mining or spell checker in editors.
Cooperation with university research groups
Red Hat supports selected doctoral students by offering them a scholarship and also resources for providing stipends to members of a student research team.
VeriFIT (FIT BUT)
Red Hat is supporting Tomáš Fiedor, member of VeriFIT research group led by prof. Tomáš Vojnar, specialises on one of the most advanced topics in static analysis of programs, namely, automated termination and resource analysis. Tools coming from this research should be able to compute precise bounds on real-world, concurrent programs with complex dynamic linked data structures like skip lists or red-black trees.
Currently, the research focus is on developing a tight combination of shape analysers (i.e. tools that infer the shape of the heap manipulated by a program), researched by VeriFIT group, together with classic techniques of analysing integer programs. The possibility of using various second order logics, namely WS1S and WS2S, for termination and bound inference, is also currently investigated.
ParaDiSe (FI MU)
The primary product of the Parallel and Distributed Systems Laboratory ParaDiSe at the Faculty of Informatics is DIVINE, an explicit-state model checker for C and C++ programs.
Since 2008, Red Hat has contributed to this effort, with the long-term goal of achieving practical, useful results. The particular focus is to build a tool which software engineers could use in their effort to produce correct and reliable software, especially for SMP (multi-core) systems.
DIVINE is the product of a small but efficient team, led by Petr Ročkai and supervised by Jiří Barnat. Petr has finished his PhD in spring 2015 (with DIVINE as the main contribution of his thesis) and currently is a full-time researcher, funded jointly by Red Hat and the Faculty of Informatics.
Furthermore, Vladimír Štill is doing his PhD, with the support of Red Hat, on DIVINE, main focus of his research is currently on extending usability of DIVINE to codebases with complex build process and on code transformations. Finally, Jan Mrázek, Henrich Lauko, and Katarína Kejstová work in our development team, as part of their work towards master or bachelor degrees. Skilled students are always welcome to join the team, as well as to select a DIVINE-related topic for their master or bachelor thesis.
ParaDiSe publications with the support of Red Hat
CRoCS (FI MU)
Centre for Research on Cryptography and Security (formerly Laboratory of Security and Applied Cryptography, established in 2006) enables both graduate and pre-graduate students to gain practical experience with current security and crypto solutions and technologies including smartcards, wireless sensor networks, disk encryption, randomness analysis and other.
The cooperation between CRoCS and Red Hat lies in the field of usable security. More specifically, the research focus is on the usability of APIs and cryptographic libraries from the point of developers and administrators lacking detailed security education.
The research is conducted by Martin Ukrop, a PhD candidate supervised by Vashek Matyáš. Currently, the emphasis is placed on X.509-capable libraries, such as OpenSSL, GnuTLS and NSS. The goal is to quantify and analyze exploits caused by incorrect API usage and help both developers use security APIs errorlessly and API designers create better interfaces less prone to misuse.