---

Academic profile

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.

Events

• STACS 2011 March 10-12, 2011, Dortmund, Germany
• GRASTA 2011 February 12-18, 2011, Dagstuhl, Germany

Recent Papers

• Clique-width: When Hard Does Not Mean Impossible
  with R. Ganian and P. Hliněný
  Accepted to STACS 2011
  
• Better algorithms for satisfiability problems for formulas of bounded rank-width
  with R. Ganian and P. Hliněný
  [PDF] [BibTeX] [Slides]
  In proceedings of FSTTCS 2010, volume 8 of LIPIcs series.
  Preprint on arxiv.org: 1006.5621
• Are there any good digraph width measures?
  with R. Ganian, P. Hliněný, J. Kneis, D. Meister, P. Rossmanith and S. Sikdar
  [PDF] [BibTeX]
  In proceedings of IPEC 2010, volume 6478 of LNCS series. © Springer-Verlag.
  Preprint on arxiv.org: 1004.1485
• Digraph Width Measures in Parametrized Algorithmics
  with R. Ganian, P. Hliněný, J. Kneis, A. Langer and P. Rossmanith
  Submitted, 34 p. (journal)
• Unified Approach to Polynomial Algorithms on Graphs of Bounded (bi-)Rank-width
  with R. Ganian and P. Hliněný
  Submitted, 29 p. (journal)
• Efficient Loop Navigation for Symbolic Execution
  with M. Trtík
  Submitted, 11 p. (conference)

Selected Journal Publications

• Qualitative Reachability in Stochastic BPA Games
  with T. Brázdil, V. Brožek and A. Kučera
  To appear in Information and Computation
  Preprint on arxiv.org: 1004.0118
• The DAG-Width of Directed Graphs
  with D. Berwanger, A. Dawar, P. Hunter and S. Kreutzer
  To appear in Journal of Combinatorial Theory, Series B.

Selected Conference Publications

• On Digraph Width Measures in Parameterized Algorithmics
  with R. Ganian, P. Hliněný, J. Kneis, A. Langer and P. Rossmanith
  [PDF] [BibTeX] [Slides]
  In proceedings of IWPEC 2009, volume 5917 of LNCS series. © Springer-Verlag.
• Qualitative Reachability in Stochastic BPA Games
  with T. Brázdil, V. Brožek and A. Kučera
  [PDF] [BibTeX] [Slides]
  In proceedings of STACS 2009, volume 3 of LIPIcs series.
  Full version with proofs: Technical report FIMU-RS-2009-01
• Clique-Width and Parity Games
  [PDF] [BibTeX] [Slides]
  In proceedings of CSL 2007, volume 4646 of LNCS series. © Springer-Verlag.
• DAG-width - Connectivity Measure for Directed Graphs
  [PDF] [BibTeX] [Slides]
  In Proceedings of SODA 2006. © SIAM
• Fast mu-calculus Model Checking when Tree-width is Bounded
  (Corrected version, including detailed algorithms)
  [PDF] [BibTeX] [Slides]
  In Proceedings of CAV 2003, volume 2725 of LNCS series. © Springer-Verlag

Older papers and the complete list can be found here.

Theses

• Algorithmic Analysis of Parity Games
  [PDF] [BibTeX]
  PhD thesis, University of Edinburgh. Submitted: January 31, 2006. Examined: May 29, 2006.
• Formal verification of sequential systems with infinitely many states
  [PS]
  Master thesis, Masaryk University, Brno, 2001.

Projects

• STANSE
  Bug-finding tool for C based on static analysis
• Institute for Theoretical Computer Science
  Formal verification, analysis, and testing of software systems [Project Supervisor]

... in the past

• RTN Games / Edinburgh
• ParaDiSe - Parallel and Distributed Systems laboratory

CV

Academic CV:[PDF]

Course information

• Static Analysis and Verification (PhD course)

Courses in the past

• Graph Theory [2006]
• Induction and Recursion [2006]
• Computability & Intractability [2005]
• CS3 Computability & Intractability [2002, 2003]
• CS3 Language Semantics and Implementation [2002, 2003]
• Formal Languages and Automata [1999,2000,2001]

Various resources

• Absence
• Personal website
• LaTeX tips
• Linux/Ubuntu/Debian tips
• Useful Windows software

---

Jan Obdržálek

Last modified: Wednesday, 14-Sep-2011 10:08:50 CEST