Tomer Kotek
My reasoning tool solver is now available online.  
Published in ICDT 2017 and available on the Dagstuhl repository:  
On the automated verification of web applications with embedded SQL. Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger. 

Published in 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 Treewidth. Tomer Kotek, Helmut Veith, Florian Zuleger. 

I am a PC member of ESSLLI 2017  
European Summer School in Logic, Language and Information, Toulouse, France. 
During the 2016 Spring semester I was a research fellow at the Simons Institute in UC Berkeley, CA.
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.
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.
Projects
Twovariable logic and its application to program verification
Verification of programs with unbounded storage size is a notoriously hard problem. Twovariable logics are especially suited as a reasoning backend to verification of such programs.
We studied verification of programs with embedded SQL commands in recent work (arXiv). We identify the subset SmpSQL of SQL and develop a complete and sound verification method for script programs with embedded SmpSQL command. The technical core of this work is the software tool FO^{2}solver which I implemented. FO^{2}solver is a modeltheorybased satisfiability checker which is competitive compared to stateoftheart reasoners such as Z3, CVC4, and Nitpick.
We have also studied the verification of imperative programs with dynamicallyallocated data structures using twovariable logics in [CKSVZ14a] and [CKSVZ14b]. For that purpose, we have developed algorithms for satisfiability checking of twovariable logics with data structures in [KSVZ15] and [KVZ16]. In [KSVZ15], our twovariable logic was a description logic ALCQIO, which is roughly the Web Ontology Language OWL2 without property inclusion axioms and datatypes.
[KVZ16]  Monadic Second Order Finite Satisfiability and Unbounded TreeWidth 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 – September 1, 2016, Marseille, France, pages 13:113:20, 2016. 
[KSVZ15]  Extending ALCQIO with Trees 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 610, 2015, pages 511522, 2015. 
[CKSVZ14b]  Shape and Content: Incorporating Domain Knowledge into Shape Analysis Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 1720, 2014., pages 124127, 2014. 
[CKSVZ14a]  Shape and Content Chapter in Integrated Formal Methods (Elvira Albert, Emil Sekerinski, eds.), pages 317, 2014, Springer. 
Verification of parameterized concurrent systems
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. We study verification of temporal properties of concurrent systems with an arbitrary number of communicating finitestate processes.
In recent work [KKWVBS16], we have collaborated with Joseph Sifakis’ group to introduce parameterization to the componentbased system design framework BIP. To our knowledge, this is the first framework that allows one to apply prominent parameterized model checking results in a systematic way.
In [AKRSV14a] we investigated the role of network topologies in the verification of concurrent systems. We have used verification reduction techniques, in which verifying properties of infinitestate systems is reduced to a small number of verification problems on finitestate systems. The verification problems on the resulting finitestate systems are solved by model checking.
[KKWVBS16]  Parameterized Systems in BIP: Design and Model Checking 27th International Conference on Concurrency Theory (CONCUR 2016) (Josée Desharnais, Radha Jagadeesan, eds.), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:130:16, 2016, Schloss Dagstuhl–LeibnizZentrum fuer Informatik. 
[AKRSV14b]  Parameterized Model Checking of Rendezvous Systems 2014, Algorithmics of Infinite State Systems workshop (FLoC 2014). 
[AKRSV14a]  Parameterized Model Checking of Rendezvous Systems Chapter in CONCUR 2014 – Concurrency Theory (Paolo Baldan, Daniele Gorla, eds.), volume 8704 of Lecture Notes in Computer Science, pages 109124, 2014, Springer Berlin Heidelberg. 
Algorithms and complexity of numeric graph parameters
In a forthcoming book chapter [Kotek16], I describe logicbase algorithms for computing numeric graph parameters. Logic is used as a broad framework for developing graph algorithms whose runtime is apriori guaranteed. In [KM15] we pushed beyond the limits of the stateoftheart in this area by developing a new framework which emits slicewise polynomialtime algorithms.
Additionally, we examined and compared models of computation for numeric graph parameters in [KMR12] and [KMR13]. Our forthcoming book chapter [KM17] and my paper [Kotek12] study the complexity of numeric graph parameters arising as evaluations of polynomials.
[Kotek16]  Logicbased computation of graph polynomials Chapter in Graph polynomials (Yongtang Shi, Matthias Dehmer, Xueliang Li, Ivan Gutman, eds.), 2016, CRC, in press. 
[KM17]  The complexity of the Tutte polynomial Chapter in Handbook of the Tutte Polynomial (Joanna A. EllisMonaghan, Iain Moffatt, eds.), 2017, CRC, in preparation. 
[KM15]  Efficient computation of generalized Ising polynomials on graphs with fixed cliquewidth Topics in Theoretical Computer Science (TTCS), 2015. 
[KMR13]  A Computational Framework for the Study of Partition Functions and Graph Polynomials Proceedings of the 12th Asian Logic Conference ’11, pages 210230, 2013. 
[Kotek12]  Complexity of Ising Polynomials Combinatorics Probability and Computing, volume 21, pages 743772, 2012. Comment: [arXiv] 
[KMR12]  A Computational Framework for the Study of Partition Functions and Graph Polynomials SYNASC, pages 365368, 2012. 
Logical definability of numeric graph parameters
Defining numeric graph parameters in logic is an essential first step towards developing algorithms for these parameters using logicbased approaches. Therefore, the question of which numeric graph parameters are definable in various logics is of high importance. We formulated the first method for proving nondefinability of numeric graph parameters in firstorder logic and monadicsecond order logic in [GKM08], [KM12b], and [KM14c]. We have also examined definability of numeric graph parameters as the counting functions of generalized colorings in [KMZ08] and [KMZ11].
[KM14c]  Connection Matrices and the Definability of Graph Parameters Logical Methods in Computer Science, volume 10, number 4, 2014. 
[KM12b]  Connection Matrices and the Definability of Graph Parameters Computer Science Logic (CSL), pages 411425, 2012. Comment: [pdf] 
[KMZ11]  On counting generalized colorings Model Theoretic Methods in Finite Combinatorics, volume 558 of Contemporary Mathematics, 2011, American Mathematical Society. Comment: [pdf] 
[KMZ08]  On Counting Generalized Colorings Computer Science Logic (CSL), pages 339353, 2008. 
[GKM08]  Evaluations of Graph Polynomials Workshop on Graph Theoretic Concepts in Computer Science (WG), pages 183194, 2008. Comment: [publishedversionpdf] 
Recurrence relations
Recurrence relations are a powerful tool for analyzing functions which count combinatorial configurations. We have studied the role of logic as a unifying framework giving rise to recurrence relations for definable numeric graph invariants in [KM09], [FKM11], [KM12a], [Kotek14], [KM14a], and [KM14b]. As a case study, we have studied recurrence relations and the related graph reconstruction problem for a specific numeric graph parameter called the edgeelimination polynomial [Kotek09] and [AKMR11].
[KM14b]  Recurrence Relations for Graph Polynomials on Biiterative Families of Graphs European Journal of Combinatorics, volume 41, pages 4767, 2014. Comment: [arXiv] 
[KM14a]  A Representation Theorem for (q)Holonomic Sequences Journal of Computer System Sciences, volume 80, pages 363374, 2014. Comment: [pdf] 
[Kotek14]  Explaining the decompositionality of monadic second order logic using applications to combinatorics 2014, Fun With Formal Methods Workshop (FLoC 2014). 
[KM12a]  A Representation Theorem for Holonomic Sequences Based on Counting Lattice Paths Fundamenta Informaticae, volume 117, number 14, pages 199213, 2012. Comment: [pdf] Note: Special issue for the 7th international conference on lattice path combinatorics and applications, Sienna, 2010 
[FKM11]  Application of logic to combinatorial sequences and their recurrence relations Model Theoretic Methods in Finite Combinatorics, volume 558 of Contemporary Mathematics, 2011, American Mathematical Society. Comment: [pdf] 
[AKMR11]  The Universal Edge Elimination Polynomial and the Dichromatic Polynomial Electronic Notes in Discrete Mathematics, volume 38, pages 77 – 82, 2011. Comment: [pdf] Note: European Conference on Combinatorics, Graph Theory and Applications (EuroComb 2011) 
[KM09]  Definability of combinatorial functions and their linear recurrence relations Fields of Logic and Computation, pages 444462, 2010. Comment: [preprintpdf] 
[Kotek09]  On the reconstruction of graph invariants Electronic Notes in Discrete Mathematics, volume 34, pages 375 – 379, 2009. Note: European Conference on Combinatorics, Graph Theory and Applications (EuroComb 2009) 
Domination polynomial
The domination polynomial is a particularly interesting numeric graph parameter. We have studied its recurrence relations, reduction formulas, and graph products. We have introduced a new graph polynomial — the bipartition polynomial — which generalizes the domination polynomial, and studied its combinatorial properties.
[KPT15]  Domination Polynomials of Graph Products Accepted to Journal of Combinatorial Mathematics and Combinatorial Computing, 2015. Comment: [arXiv] 
[DKPT15]  Bipartition polynomials, the Ising model and domination in graphs Discussiones Mathematicae Graph Theory, volume 35, number 2, pages 335353, 2015. 
[KPT13]  SubsetSum Representations of Domination Polynomials Graphs and Combinatorics, volume 30, pages 647660, 2013, Springer Japan. 
[KPSTT12]  Recurrence Relations and Splitting Formulas for the Domination Polynomial Electronic Journal of Combinatorics, volume 19, 2012. Comment: [arXiv] 
Machine learning
We studied the multiclass classification problem using SVMs. The approach we used was reductions of the classification problem to a single application of a binary SVM.
[EKPY06]  On Multiclass Classification via a Single Binary Classifier Comment: IBM report, 2006 
Address:
Tomer Kotek
Technische Universität Wien
Institut für Informationssysteme 184/4
Favoritenstraße 9–11
1040 Wien
Austria
Room:  HD 03 05 (how to get there) 
Phone:  +43 (1) 58801 – 184 835 
Email:  ta.etysrofnull@ketok 
Web:  http://forsyte.at/~kotek/ 