Tomer Kotek

My reasoning tool fo2-solver is now available online.
Available on arXiv:
On the automated verification of web applications with embedded SQL.
Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger.
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 currently 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

Two-variable logic and its application to program verification

Verification of programs with unbounded storage size is a notoriously hard problem. Two-variable 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 FO2-solver which  I implemented. FO2-solver is a model-theory-based satisfiability checker which is competitive compared to state-of-the-art reasoners such as Z3, CVC4, and Nitpick.

We have also studied the verification of imperative programs with dynamically-allocated data structures using two-variable logics in [CKSVZ14a] and [CKSVZ14b]. For that purpose, we have developed algorithms for satisfiability checking of two-variable logics with data structures in [KSVZ15] and [KVZ16]. In [KSVZ15], our two-variable 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 Tree-Width
Tomer Kotek, Helmut Veith, Florian Zuleger
25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 – September 1, 2016, Marseille, France, pages 13:1-13:20, 2016.
[bibtex] [doi]
[KSVZ15] Extending ALCQIO with Trees
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 511-522, 2015.
[bibtex] [pdf] [doi]
[CKSVZ14b] Shape and Content: Incorporating Domain Knowledge into Shape Analysis
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17-20, 2014., pages 124-127, 2014.
[bibtex]
[CKSVZ14a] Shape and Content
Diego Calvanese, Tomer Kotek, Mantas Šimkus, Helmut Veith, Florian Zuleger
Chapter in Integrated Formal Methods (Elvira Albert, Emil Sekerinski, eds.), pages 3-17, 2014, Springer.
[bibtex] [pdf] [doi]

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 finite-state processes.

In recent work [KKWVBS16], we have collaborated with Joseph Sifakis’ group to introduce parameterization to the component-based 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 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.

[KKWVBS16] Parameterized Systems in BIP: Design and Model Checking
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis
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:1-30:16, 2016, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf]
[AKRSV14b] Parameterized Model Checking of Rendezvous Systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith
2014, Algorithmics of Infinite State Systems workshop (FLoC 2014).
[bibtex]
[AKRSV14a] Parameterized Model Checking of Rendezvous Systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith
Chapter in CONCUR 2014 – Concurrency Theory (Paolo Baldan, Daniele Gorla, eds.), volume 8704 of Lecture Notes in Computer Science, pages 109-124, 2014, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]

Algorithms and complexity of numeric graph parameters

In a forthcoming book chapter [Kotek16], I describe logic-base algorithms for computing numeric graph parameters. Logic is used as a broad framework for developing graph algorithms whose runtime is a-priori guaranteed. In [KM15] we pushed beyond the limits of the state-of-the-art in this area by developing a new framework which emits slice-wise polynomial-time 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] Logic-based computation of graph polynomials
Tomer Kotek
Chapter in Graph polynomials (Yongtang Shi, Matthias Dehmer, Xueliang Li, Ivan Gutman, eds.), 2016, CRC, in press.
[Book]
[KM17] The complexity of the Tutte polynomial
Tomer Kotek, Johann A. Makowsky
Chapter in Handbook of the Tutte Polynomial
(Joanna A. Ellis-Monaghan, Iain Moffatt, eds.)
, 2017, CRC, in preparation.
[Book]
[KM15] Efficient computation of generalized Ising polynomials on graphs with fixed clique-width
Tomer Kotek, Johann A. Makowsky
Topics in Theoretical Computer Science (TTCS), 2015.
[bibtex]
[KMR13] A Computational Framework for the Study of Partition Functions and Graph Polynomials
T. Kotek, J. A. Makowsky, E. V. Ravve
Proceedings of the 12th Asian Logic Conference ’11, pages 210-230, 2013.
[bibtex]
[Kotek12] Complexity of Ising Polynomials
T. Kotek
Combinatorics Probability and Computing, volume 21, pages 743-772, 2012.
Comment: [arXiv]
[bibtex] [pdf]
[KMR12] A Computational Framework for the Study of Partition Functions and Graph Polynomials
Tomer Kotek, Johann A. Makowsky, Elena V. Ravve
SYNASC, pages 365-368, 2012.
[bibtex] [pdf]

Logical definability of numeric graph parameters

Defining numeric graph parameters in logic is an essential first step towards developing algorithms for these parameters using logic-based 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 non-definability of numeric graph parameters in first-order logic and monadic-second 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
Tomer Kotek, Johann A. Makowsky
Logical Methods in Computer Science, volume 10, number 4, 2014.
[bibtex]
[KM12b] Connection Matrices and the Definability of Graph Parameters
T. Kotek, J.A. Makowsky
Computer Science Logic (CSL), pages 411-425, 2012.
Comment: [pdf]
[bibtex] [pdf]
[KMZ11] On counting generalized colorings
T. Kotek, J.A. Makowsky, B. Zilber
Model Theoretic Methods in Finite Combinatorics, volume 558 of Contemporary Mathematics, 2011, American Mathematical Society.
Comment: [pdf]
[bibtex] [pdf]
[KMZ08] On Counting Generalized Colorings
T. Kotek, J.A. Makowsky, B. Zilber
Computer Science Logic (CSL), pages 339-353, 2008.
[bibtex]
[GKM08] Evaluations of Graph Polynomials
B. Godlin, T. Kotek, J.A. Makowsky
Workshop on Graph Theoretic Concepts in Computer Science (WG), pages 183-194, 2008.
Comment: [published-version-pdf]
[bibtex] [pdf]

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 edge-elimination polynomial [Kotek09] and [AKMR11].

[KM14b] Recurrence Relations for Graph Polynomials on Bi-iterative Families of Graphs
Tomer Kotek, Johann A Makowsky
European Journal of Combinatorics, volume 41, pages 47-67, 2014.
Comment: [arXiv]
[bibtex] [pdf]
[KM14a] A Representation Theorem for (q-)Holonomic Sequences
T. Kotek, J. A. Makowsky
Journal of Computer System Sciences, volume 80, pages 363-374, 2014.
Comment: [pdf]
[bibtex] [pdf]
[Kotek14] Explaining the decompositionality of monadic second order logic using applications to combinatorics
Tomer Kotek
2014, Fun With Formal Methods Workshop (FLoC 2014).
[bibtex]
[KM12a] A Representation Theorem for Holonomic Sequences Based on Counting Lattice Paths
T. Kotek, J.A. Makowsky
Fundamenta Informaticae, volume 117, number 1-4, pages 199-213, 2012.
Comment: [pdf]
Note: Special issue for the 7th international conference on lattice path combinatorics and applications, Sienna, 2010
[bibtex] [pdf]
[FKM11] Application of logic to combinatorial sequences and their recurrence relations
E. Fischer, T. Kotek, J.A. Makowsky
Model Theoretic Methods in Finite Combinatorics, volume 558 of Contemporary Mathematics, 2011, American Mathematical Society.
Comment: [pdf]
[bibtex] [pdf]
[AKMR11] The Universal Edge Elimination Polynomial and the Dichromatic Polynomial
I. Averbouch, T. Kotek, J.A. Makowsky, E. Ravve
Electronic Notes in Discrete Mathematics, volume 38, pages 77 – 82, 2011.
Comment: [pdf]
Note: European Conference on Combinatorics, Graph Theory and Applications (EuroComb 2011)
[bibtex] [pdf]
[KM09] Definability of combinatorial functions and their linear recurrence relations
T. Kotek, J.A. Makowsky
Fields of Logic and Computation, pages 444-462, 2010.
Comment: [preprint-pdf]
[bibtex] [pdf]
[Kotek09] On the reconstruction of graph invariants
T. Kotek
Electronic Notes in Discrete Mathematics, volume 34, pages 375 – 379, 2009.
Note: European Conference on Combinatorics, Graph Theory and Applications (EuroComb 2009)
[bibtex]

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
Tomer Kotek, James Preen, Peter Tittmann
Accepted to Journal of Combinatorial Mathematics and Combinatorial Computing, 2015.
Comment: [arXiv]
[bibtex]
[DKPT15] Bipartition polynomials, the Ising model and domination in graphs
Markus Dod, Tomer Kotek, James Preen, Peter Tittmann
Discussiones Mathematicae Graph Theory, volume 35, number 2, pages 335-353, 2015.
[bibtex] [pdf]
[KPT13] Subset-Sum Representations of Domination Polynomials
Tomer Kotek, James Preen, Peter Tittmann
Graphs and Combinatorics, volume 30, pages 647-660, 2013, Springer Japan.
[bibtex] [pdf] [doi]
[KPSTT12] Recurrence Relations and Splitting Formulas for the Domination Polynomial
T. Kotek, J. Preen, F. Simon, P. Tittmann, M. Trinks
Electronic Journal of Combinatorics, volume 19, 2012.
Comment: [arXiv]
[bibtex] [pdf]

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
Ran El-Yaniv, Tomer Kotek, Dmitry Pechyony, Elad Yom-Tov
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/

kotekIMG_1962


Latest News

WAIT 2016 in Vienna

The third WAIT workshop on induction is held between 17-18 November at the TU Wien. Details are available on the workshop page.

Continue reading

Two papers at POPL’17

Two papers co-authored by researchers from our group have been accepted for POPL’17: “Coming to Terms with Quantified Reasoning” by Simon Robillard, Andrei Voronkov, and Laura Kovacs; and “A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms” by Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder

Continue reading

Helmut Veith Stipend

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

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.

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

Full news archive