Antonín Kučera

Research interests: Modelling and verification of infinite-state systems, methods and algorithms for analyzing stochastic processes, applications of game theory in computer science, modal and temporal logics.


Achim Blumensath

Research interests: Algorithmic model theory, model theory for monadic second-order logic, automata theory and algebraic language theory, graph theory and combinatorics

Tomáš Brázdil

Research interests: Algorithmic analysis of stochastic systems, game theory with applications in computer science, probabilistic temporal logics

Petr Hliněný

Research interests: Structural graph theory, geometric and topological graph theory, graph crossing numbers, parameterized algorithms and complexity, algorithmic metatheorems.

Jan Obdržálek

Research interests: Structural graph theory, parameterized complexity, infinite games on graphs (esp. parity games), mu-calculus, verification of infinite state systems, software verification, OpenMP for Java.

Vojtěch Řehák

Research interests: Formal modelling and verification of real systems (e.g. HW design, network protocol), performance analysis, stochastic and real time models, infinite state models, modal and temporal logics.

Jan Strejček

Research interests: Formal methods for program analysis and verification (static analysis, abstract interpretation, symbolic execution, model checking), modal and temporal logics, automata over infinite words, translation of LTL to automata, SMT solving.


Bodhayan Roy

Research interests: Combinatorial and computational geometry

PhD students

František Blahoudek

Research interests: Automata over infinite words.
Supervisors: Mojmír Křetínský, Jan Strejček

Onur Cagirici

Research interests: Graph theory, combinatorial and computational geometry.
Supervisor: Petr Hliněný

Marek Derňár

Research interests: Graph theory - crossing numbers.
Supervisor: Petr Hliněný

Marek Chalupa

Research interests: Program analysis.
Supervisor: Jan Strejček

Martin Jonáš

Research interests: SMT solving.
Supervisor: Jan Strejček

David Klaška

Research interests: Complexity of Consumption Games.
Supervisor: Antonín Kučera

Ľuboš Korenčiak

Research interests: Formal modelling and verification of distributed systems and countinuous time stochastic systems.
Supervisor: Antonín Kučera, Vojtěch Řehák

Dominik Velan

Research interests: Infinite state stochastic systems.
Supervisor: Tomáš Brázdil

Martina Vitovská

Tesearch interests: Program Analysis.
Supervisor: Jan Strejček

Bachelor/Master students

Tomáš Jašek

Topic: Program Analysis
Supervisor: Jan Strejček

Mikuláš Klokočka

Topic: Automata over Infinite Words
Supervisor: František Blahoudek, Jan Strejček

Dominika Krejčí

Topic: SMT solving
Supervisor: Martin Jonáš, Jan Strejček

Tomáš Lamser

Topic: Security Games
Supervisor: Antonín Kučera

Peter Navrátil

Topic: SMT solving
Supervisor: Martin Jonáš, Jan Strejček

Miriama Sasaráková

Topic: Automata over Infinite Words
Supervisor: František Blahoudek, Jan Strejček

Ondřej Slámečka

Topic: Efficient Generation of Multiway Cuts
Supervisor: Petr Hliněný

Kateřina Sloupová

Topic: SMT solving
Supervisor: Martin Jonáš, Jan Strejček

Mário Uhrík

Topic: Stochastic Models
Supervisor: Ľuboš Korenčiak

Tatiana Zbončáková

Topic: Automata over Infinite Words
Supervisor: František Blahoudek, Jan Strejček

Filip Pokrývka

Topic: FO model checking of geometric graphs
Supervisor: Petr Hliněný

Matúš Bezek

Topic: DAG-depth of directed graphs
Supervisor: Petr Hliněný

Former members

PhD students
  • Tomáš Babiak
    Thesis: Translation of Linear Temporal Logic to Omega-Automata (2017)
  • Jakub Gajarský
    Thesis: Algorithmic metatheorems for restricted classes of graphs (2016)
  • Jan Krčál
    Thesis: Formal Analysis of Discrete-Event Systems with Hard Real-Time Bounds (2013)
  • Jan Křetínský
    Thesis: Modal Transition Systems: Extensions and Analysis (2014)
  • Ondrej Moriš (Suspended)
  • Petr Novotný
    Thesis: Controller Synthesis for Resource-Aware Systems (2015)
  • Jiří Slabý
    Thesis: Automatic Bug-finding Techniques for Large Software Projects (2014)
  • Marek Trtík
    Thesis: Symbolic Execution and Program Loops (2014)
  • Robert Ganian
    Thesis: Parameterized Algorithms on Width Parameters of Graphs (2012)
Bachelor/Master students
people.txt · Last modified: 2018/03/19 17:48 by Jan Strejček