Current areas of PhD study

Efficient formal analysis and verification of programs written in imperative languages

In practice, the currently dominating approach to verification of programs written in imperative languages (such as C, C#, Java, etc.) is testing. A given program is repeatedly run on a large selection of input data, and the outcomes of these trial runs are evaluated and analysed. The main disadvantages of testing are its expensiveness and principal unreliability.

A more sophisticated approach to program analysis and verification is based on formal methods, which allow to discover certain type of errors or prove their absence just by analyzing the source code of a given program. The main disadvantage of formal methods is their computational complexity, which often does not permit to analyze programs of a real size.

The topics of PhD theses in this area are focussed on developing practically usable formal methods that are applicable to real-world programs written in imperative languages. The expected outcomes are new theoretical concepts and their implementation into an integrated software tool.

This area was formulated in cooperation with ANF DATA company.

Supervisor: prof. RNDr. Antonín Kučera, PhD
Co-supervisor: Mgr. Jan Obdržálek, PhD (contact person)

Advanced techniques in modelling and verification of network-based services

The aim of this research topic is to develop rigorous methods for modelling and analysis of various network-based services. The major problem is that while the functionality specifications (protocols) are often formally described, they are not complete and leave space for different interpretation in the implementation phase. Therefore, functionality of actual implementations is influenced by only vaguely defined assumptions, which lead to incompatibility and instability of a system composed of two or more interacting components.

We study formalisms for network-based system specification at a very early stage of design. Variety of studies has been done on Message Sequence Charts (MSC) formalism in this research area. Even though MSC is formally specified in ITU Recommendation Z.120, most of the theoretical results deals with some subsets of this formalism only. On the other hand, there are many undecidability results related to the MSC in its full expressive power.

The aim of this research is to find a subset of MSC (or its useful modification) such that it can express important design features and, at the same time, it preserves decidability of significant verification questions.

This research area is explored in a direct cooperation with ANF DATA company. Hence, new approaches and ideas can be implemented and immediately tested in practice. Even a small progress leading to detecting and avoiding the aforementioned problem (at least in some situations) can have a huge practical impact.

Supervisor: prof. RNDr. Mojmír Křetínský, CSc.
Co-supervisor: RNDr. Vojtěch Řehák, PhD (contact person)

Algorithms and tools for analysis of dynamically allocated memory

A substantial part of today's software products works with dynamic memory allocation. Such software (mainly in its development phase) is prone to contain specific errors that may diminish the performance or even cause a breakdown of the system. Two examples of the most typical errors are memory leaking, when a programmer forget to deallocate a part of memory which is no longer needed, and NULL pointer dereference leading to an immediate software failure. Such an error is hard to detect and fix, especially if it does not occur during each execution of the program.

This is the reason for the current intensive research in the area of formal methods for automated analysis of dynamically allocated memory. These methods allow to find potential bugs of the considered type, or verify that the program does not contain such bugs. The results of the analysis can be also used in other ways, for example for code optimization (it is known that timeous deallocation of unused memory in Java code can save approximately 39% of memory in average).

PhD theses in this area can be focused on design of new algorithms for analysis of dynamically allocated memory (potentially combined with other methods of code analysis), searching for new application of results produced by this analysis (including error detection, code verification, optimization, etc.) and development of practical tools for standard programming languages. We assume that PhD theses focused on development of practical tools arouse interest of some industrial partners of our faculty or other software companies.

Supervisor: prof. RNDr. Mojmír Křetínský, CSc.
Co-supervisor: doc. RNDr. Jan Strejček, PhD (contact person)

Natural Language Processing and Artificial Intelligence

The research is directed namely to: text corpora and corpus tools, syntactic and semantic analysis of natural language, dialogue and question-answering systems, computer lexicography together with machine readable dictionaries, and last but not least, machine translation. The field of Natural Language Processing is closely related to the issues of AI and it intertwines with knowledge representation which comprises semantic networks, logical calculi (deduction systems) and various types of ontologies. Current issues of the Semantic Web also belong here.

From the methodological point of view this is an attractive area, in which we encounter difficult problems, however, their solution can make human-computer communication easier. Presently it can be characterized as exclusively 'one-way', i.e. it means that humans have to have the sufficient knowledge about the structure of the software to be able to use computers on a reasonable level. The goal we want to reach, however, is rather a 'two-way' communication, which will make computers closer to humans who do not possess the mentioned knowledge. The contemporary research paradigms exploit rule-based and statistical approaches, or the hybrid ones.

The topics of the dissertations in this area are oriented to the solutions of the problems mentioned above. In the dissertations the students are expected to seek for new theoretical approaches and techniques in Natural Language Processing as well as their implementation having the form of the tools usable in further research or in practical applications.

Those topics have developed in the framework of the NLP Laboratory which came to the existence at the Faculty of Informatics in years 1997-8. Presently we are starting the cooperation with the Seznam Company, thus topics can be formulated that are related to the cooperation with this industrial partner. Another interesting opportunity is a research cooperation with the British Company Lexmaster Class. The papers based on successful dissertations can be published in the proceedings of the international conferences related to NLP and AI and the postgraduates are expected to present them there.

Supervisor: doc. PhDr. Karel Pala, CSc.
Co-supervisors: doc. RNDr. Aleš Horák, PhD, Mgr. Pavel Rychlý, PhD (contact persons)

Speech processing, dialogue systems and assistive technologies

Speech processing, covering speech recognition and synthesis, belongs to the most interesting fields of computer science, producing applications that will be even more important in a near future. Exploiting speech technologies, dialogue systems form intelligent human-computer interface primarily based on speech. Assistive technologies aim to the applications supporting quality of the life, especially in helping handicapped people.

In this field, the topics of the theses may be related to specific problems that are solved within the Laboratory of Speech and Dialogue. For instance, dialogue generation of graphical objects and www pages, speech synthesis and recognition, assistive technologies; however, all research ideas are welcome.

Supervizor: doc. RNDr. Ivan Kopeček, CSc.

Advanced searching methods for digital data

Our research focuses on fast similarity search in large data collections. Standard techniques based on centralized directories lack the scalability needed to process the exponential growth of data of current digital explosion. On the other hand, distributed systems (such as GRID or peer-to-peer networks) offer the necessary resources. We concentrate our efforts on both structured and unstructured distributed systems. A very important area of research is the specification of similarity measures, i.e. the metrics used to compare pieces of data. The choice of an appropriate metric function is crucial not only for the quality of the searching results but also for its response time.

Possible topics for PhD theses:

  • Ranking and Relevance Feedback in Image Retrieval
  • Similarity Search Architectures for WEB Databases
  • Self-Organized Search Networks
  • Computational Advertising
  • Clustering and Categorization in Metric Spaces
  • Similarity Search Applications: video, audio, music
  • Similarity Searching: Beyond the Metric Space
  • Data Cleaning and Integration
  • Collaborative Filtering
  • Performance Tuning on Distributed Hardware Infrastructures
  • Approximative Similarity Search
  • Dimensionality Reduction Techniques

Supervisor: prof. Ing. Pavel Zezula, CSc.

Structural and topological graph theory

We study applications of deep theoretical results of structural and topological graph theory in design of new faster algorithms. This is a theoretical topic with expected collaboration with some of the leading international experts in these areas. We propose the following specific research topics, but other related topics can be arranged on demand:

  • Non-traditional width parameters of graphs, e.g. rank-width, DAG-width, or others. Their mathematical properties, and algorithmic use.
  • The crossing number of a graph: structure of crossing-critical graphs, efficient computation/approximation of the crossing number for graphs close to planarity.
  • Other problems of structural and topological graph theory related to algorithms and complexity.

Supervisor: doc. RNDr. Petr Hliněný, PhD

Parameterized complexity and algorithms

We focus of question and problems in a rather new CS area of so called parameterized complexity. This theory provides a new look at difficulty of many NP-hard problems, allowing for efficient solutions under additional restrictions (parametrization). This is, again, a theoretical field with expected collaboration with some of the leading international experts. We propose the following specific research topics, but other related topics can be arranged on demand:

  • Applying results of structural graph theory in parameterized complexity and in parameterized algorithm design.
  • Studying new "width" parameters of graphs and digraphs, and comparing their algorithmic strength.
  • Use of structural graph theory and suitable decompositions of graphs in faster and memory-limited route planning algorithms on huge graphs.

Supervisor: doc. RNDr. Petr Hliněný, PhD

Triangulated models for haptics and virtual reality

Triangulated models have been the main tool for representation of geometric objects since the very beginning of computer graphics. There are several categories: first, 2D triangulations, which can be used for modeling of terrains or other flatland objects; they can be also made in a parametric space and mapped to a surface of a geometric model. Second, 3D triangulations or tetrahedronizations used to model geometric bodies. Third, surface triangulated models, obtained by surface reconstruction from scattered points or by piecewise linear interpolation of various functional representations. Many algorithms and methods for all these models have been developed; most of them work well in the context of computer graphics and its typical applications. However, if the input data or application requirements are large and moving, with non-geometric criteria of triangle optimality for soft deformations and other shape changes, the triangulated models topics are far less solved and known solutions far less satisfactory for new application areas.

The main goal of the research is to develop algorithms and methods suitable for VR simulations and to use them in this context. The developed solution will be used mainly in the context of multimodal human computer interaction methods, namely for training applications.

Possible topics for PhD theses:

  • Algorithms for fast location on the surface of geometric models.
  • Local refinement and coarsening of triangular surface during a haptic interaction.
  • Triangulated models based on kinetic data; research of non-geometrical criteria of optimality.
  • Modeling of deformations and evolution of geometrical objects.
  • Path planning/searching in the VR applications in partly known or unknown environment, with possibilities to re-plan rapidly the path in case of objects shape changes.
  • Fast frame-to-frame collision detection of triangulated models as an input for correct force-feedback calculation.
  • Development of fine rigid as well as flexible tools with dense triangulated surface structures and their application to fine grained haptic interactions.
  • Design and implementation of detailed surface models for VR scenes, allowing simulation of interactions of a type human controlled tools interacting with rigid and soft surface models.

Supervisor: doc. Ing. Jiří Sochor, CSc.

Analysis of cell images in optical microscopy

Modern molecular biology is primarily concerned with the studies of structure, function and dynamics of cellular components. For this purpose it mainly uses optical microscopy that enables capturing of spatial (3D) image data as well as time course of cellular processes in live cells without their damage (in natural conditions). Motivation of this research is the effort to describe cellular processes that lead to deleterious (especially cancer) human diseases and, based on this knowledge, to develop new efficient diagnostic as well as therapeutic approaches.

Because these studies produce huge multi-dimensional image data that must be captured, digitized and processed using computer in the appropriate manner, they can't be realized without experts in the field of digital image processing. Such help is offered to molecular biologists by the Centre for Biomedical Image Analysis at FI MU. This Centre has not only computer equipment available but also molecular biology laboratories for the preparation of cells and optical laboratories equipped with unique automated microscopes driven by our own software. Hence, the Centre handles the whole process of cell sample studies starting with taking of the cell sample in hospital and ending with the evaluation of the results produced by computer.

Participation on the activities of the Centre is possible also in the way of PhD studies. In this case not only new method proposals are expected as output but also their functional implementation in the format compatible with the existing library that is continually being developed in this Centre.

More specifically attention is paid mainly to the tasks in the area of segmentation of cells and their components, in the case of live cells also to the tracking of moving objects inside the cell as well as movement of the cell itself. We usually make an effort to automate and optimize the developed methods to large extent with respect to quality and/or quantity of produced results. We also pay attention to the simulation of image formation in optical systems: creating models of the cells, of the blur caused by optical system, of the electronic noise and of the other artifacts in order to have the possibility of assessing the reliability of the developed image analysis methods as well as to find the ways of correcting the mentioned imperfections using hardware and/or software means.

The prerequisites for the work on these topics is the will to learn something new from other fields (especially optics and molecular biology) and to communicate with colleagues with these backgrounds who are employed also directly by the Centre. It is expected that the student typically spends one semester in a similar centre abroad during the PhD studies.

Supervisor: prof. RNDr. Michal Kozubek, PhD
Co-supervisors: doc. RNDr. Pavel Matula, PhD, doc. RNDr. Petr Matula, PhD, RNDr. David Svoboda, PhD (contact persons)

Models for programmability and traceability of self-organizing communication systems

This dissertation work topic is to develop programming models, that allow modification of the self-organizing systems behavior without disrupting basic self-organizing constraints. The ability to modify the behavior will allow to create more flexible communication systems, where user can modify properties like trade-offs between speed of network establishment (within given requirements) and it properties (like real transmission rate, latency, level of robustness based on link redundancy). The work will focus especially on finding such models, that also allow to understand behavior of the self-organizing systems being established and that provide at least basic means for tracing and debugging. This means they need to enable monitoring of system behavior during self-organization process and provide reproducible environment to reproduce and analyze errors and unexpected states. Results of such a research can be integrated into current CoUniverse Framework.

Time frame: The work could start in academic year 2008/2009 by doing bibliographical research and specification of requirements for the model. 2009/2010: proposals of first generation of the programming model, that will guarantee global properties of the self-organizing system. 2010/2011: Work on tracing and debugging abilities, second generation of the model, experiments and simulations. 2011/2012: Finalization of experiments, evaluation and finalization of Ph.D. thesis.

Supervisor: prof. RNDr. Luděk Matyska, CSc.
Co-supervisor: RNDr. Petr Holub, PhD, (contact person)

Quantum information processing - quantum algorithms, automata, cryptography

Quantum information processing is a new trend in the field of information processing, computation, communication and security. Specific laws of quantum mechanics and properties of microscopic quantum world can be harnessed to solve problems that cannot be solved with classical computers or to solve them more efficiently.

The research focuses namely on quantum finite automata, quantum algorithms, design of quantum circuits and protocols, and on various problems of quantum cryptography - quantum key generation, encryption, authentication, anonymity etc.

Topics of PhD theses can also be related to specific problems of the theory of quantum information, quantum error-correction codes, quantum entanglement etc.

Students are expected to join the Laboratory of Quantum Information Theory and Cryptography, The laboratory regularly organizes research and "hot topics" seminars where the new results are presented. The lab is one of the organizers of international workshop CEQIP (Central European Quantum Information Processing) held each year in the Czech Republic.

Supervisor: prof. RNDr. Jozef Gruska, DrSc.
Co-supervisors: RNDr. Jan Bouda, PhD, doc. Mgr. Mario Ziman, PhD, prof. RNDr. Tomáš Tyc, PhD (contact persons)

Security Machine Learning

Laboratories of Knowledge Discovery & Security and Applied Cryptography of the Faculty of Informatics and AVG search for 2 positions of Security Machine Learning Experts. At least one of these positions is sought at the Master graduate level (starting PhD student) and at most one might be for a postdocs. The selected candidate(s) for PhD studies will be offered a part-time(about 50%) position at AVG and also enter the PhD program with the Knowledge Discovery Group. Strong interaction with members of the Laboratory of Security and Applied Cryptography and with AVG is expected.

Required Skills
- Familiarity with machine learning and data mining.
- Scripting Programming Skills.
- Knowledge of Databases.
- Ability to work and analyze large datasets.

Desired Skills
- Familiarity with Windows, Windows Internals and Windows tools.
- Knowledge of Windows architecture, registry functionality and kernel internals.
- Understanding of modern anti‐virus and behavior-based anti‐malware technologies.
- Knowledge and experience in Perl and C++.

- Analysis of binary characteristics using Bayesian models to identify new malware families.
- Daily analysis of large data sets by utilizing machine learning models.
- Cooperation with malware researchers to identify false positive/negative cases.
- Classification of known malware and legitimate software samples, clustering and training of the system for better automated classification.
- Delivery of binary characteristics that identify malware under a given false positive condition to malware researchers.
- More on the basics of technology used can be found here.

Supervisor: doc. RNDr. Lubomír Popelínský, PhD

Security of payment protocols

1 PhD student sought:

We investigate security of protocols proposed in our existing research with the Y Soft Corporation. A basic suite of these protocols has been designed recently, and is currently under independent (human) evaluation and also extended by various supporting protocols and settings.

We are looking for a PhD student interested in the following three related areas:
1. Considerations and settings of cryptographic primitives for the first design of the protocol suite for secure payments.
2. Automated verification of selected prototols, to be undertaken in a close cooperation with Dr. Vojtech Rehak, ITI.
3. Participation in prototype development and testing, as well as write-up of an open standard with the protocols‘ specification.

Start date – September 2012.

Supervisor: prof. RNDr. Václav Matyáš, M.Sc., PhD

Methods for the design and development of reliable software architectures

In both research and industrial development, a high number of methods exists that guide the the development of functionally correct systems (including formal verification or testing). However, the functional correctness is only one of many quality attributes of software systems - next to the performance, reliability, security, energy consumption, maintainability, and many others. With the increasing complexity of software systems, and their architectures in particular, new techniques are needed for the quality-driven design and development of these systems, targeting the desired system qualities.

The topics of the PhD theses in this area focus on one selected quality attribute - the reliability - and aim at the development of methods for the reliability-driven design and development of large-scale software systems, maximizing system reliability. With the method development, we understand both the theoretical design of the methods, and their implementation and/or integration into an existing tool, including the practical evaluation of the results on a number of case studies of real systems.

Supervisor: doc. RNDr. Tomáš Pitner, Ph.D.
Co-supervisor: Ing. RNDr. Barbora Bühnová, Ph.D. (full capacity at this moment)