Tomer Kotek


  Accepted to CONCUR 2016:
Parameterized Systems in BIP: Design and Model Checking.
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis.
  Accepted to CSL 2016:
Monadic Second Order Finite Satisfiability and Unbounded Tree-width.
Tomer Kotek, Helmut Veith, Florian Zuleger.
  I am a PC member of ESSLLI 2017, European Summer School in Logic, Language and Information, Toulouse, France.


I am a postdoc at the Forsyte group of TU Vienna. My research aims at bringing tools and methods from logic to computer science. I am interested in particular in applications of finite model theory to complexity, combinatorics, formal methods and knowledge representation. My research philosophy places a strong emphasis on interdisciplinarity. Different computer science communities, such as the verification community, the graph algorithms community, the databases community and the knowledge representation community, have studied closely related computational tasks on graphs and finite structures. Most of my works combine ideas and techniques from at least two different research communities.

See some recent projects below.

I did my Ph.D. at the computer science department of the Technion in Haifa with Prof. Johann Makowsky. In my Ph.D. dissertation Definability of Combinatorial Functions and in later work, I have studied the logical definability, the computational complexity and the combinatorial properties of graph invariants, and how they interrelate.


CV from November 2014.

Recent projects:

Content analysis of programs.

The manipulation and storage of complex information in imperative programming languages is often achieved by dynamic data structures. The verification of programs with dynamic data structures, however, is notoriously difficult, and is a highly active area of current research. The verification community has studied dynamic data structures primarily in a bottom-up way by analyzing pointers and the shapes induced by them. Many real world programs however manipulate complex data whose structure and content is most naturally described by formalisms from object oriented programming and databases. I look at the verification of programs with dynamic data structures from the perspective of content representation. In this perspective, data structures in the heap form an in-memory database. I use this perspective to analyze and prove the correctness of programs with dynamic data structures.
I am collaborating with leading researchers from both the verification community and the knowledge representation community to develop a verification methodology that employs description logics for formulating and verifying content specifications of pointer-manipulating programs.

Verification of systems with many processes.

Many concurrent systems consist of an arbitrary number of identical processes running in parallel, possibly in the presence of an environment or control process. Correctness properties are expected to hold irrespective of the number of participating processes. I study verification of temporal properties of concurrent systems with an arbitrary number of communicating finite-state processes. I investigate the role of network topologies in the verification of concurrent systems. In recent work I have used reduction techniques, where the problem of verifying properties of infinite-state systems is reduced to a small number of verification problems on finite-state systems. The verification problems on the resulting finite-state systems are solved by model checking.

Reasoning over logics with trees.

Reasoning over expressive graph logics with reachability has received considerable attention in several research communities, including finite model theory, software verification and knowledge representation. My work on content analysis of programs as well as on verification of concurrent systems have in common that they rely on decidable logics with reachability, since reachability is natural when axiomatizing both data structures and network topologies. Development of logics with low reasoning complexity and suitable expressive power, including in particular reachability, is a major challenge due to the delicate balance between high expressivity and low complexity. I have developed and continue to explore logics which can express the reachability requirements of data structures and network topologies.

Tomer Kotek
Technische Universität Wien
Institut für Informationssysteme 184/4
Favoritenstraße 9–11
1040 Wien

Room: HD 03 05 (how to get there)
Phone: +43 (1) 58801 – 184 835
Email: ta.etysrofnull@ketok



Latest News

LogicLounge in memoriam Helmut Veith

Will robots take away your job? In memory of Helmut Veith, this year’s Conference on Computer Aided Verification (CAV), which takes place in Toronto, will feature a LogicLounge on the effect of automation and artificial intelligence on our jobs. The LogicLounge discussion series was initiated during the Vienna Summer of Logic 2014 and aims to […]

Continue reading

Marijana Lazić wins ZONTA mobility stipend

Marijana Lazić won the “ZONTA CLUB WIEN I – TU-Mobilitätsstipendium” for her research in the intersection of computer-aided verification and distributed computing theory. The stipend will support her in attending international conferences in the concerned research areas. Supported by ZONTA, she is already on a trip to the US and Canada to attend this year’s […]

Continue reading

Questions answered by Leslie Lamport

Leslie Lamport is going to answer questions about a Mathematical View of Computer Systems in Informatikhörsaal on Tuesday at 6pm. Check the announcement at the VCLA website and do not forget to watch the lecture beforehand.

Continue reading

Laura Kovács joins FORSYTE as full professor

We welcome Laura Kovács, who joined the FORSYTE group as a full professor of computer science in April 2016. Laura also holds a part-time associate professorship at the Chalmers University of Technology, Sweden. Her research deals with the design and development of new theories, technologies, and tools for program analysis, with a particular focus on […]

Continue reading

Full news archive