- 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.
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.
Technische Universität Wien
Institut für Informationssysteme 184/4
|Room:||HD 03 05 (how to get there)|
|Phone:||+43 (1) 58801 – 184 835|