Igor Khmelnitsky

I am a PhD student in the LMF (previously known as th LSV) in ENS Paris-Saclay, under the supervision of Alain Finkel and Serge Haddad. My research is currently mainly focused on verification of infinite state systems, such as Petri nets, recursive Petri nets, well structured transition systems, etc. Since these type of systems can be hard to verify using the classical algorithms, I began trying to introduce machine learning technique to the verification of theses systems.

A complete CV in PDF form

Research

Publications

Journal:

• A. Finkel, S. Haddad, and I. Khmelnitsky. Coverability, Termination, and Finiteness in Recursive Petri Nets, in Fundamenta Informaticae, To be published in 2021
• A. Finkel, S. Haddad, and I. Khmelnitsky. Commodification of Accelerations for the Karp and Miller Construction, , Discrete Event Dynamic Systems, 2020.

Inter national Conferences:

2021

• B. Barbot, B. Bollig, A. Finkel, S. Haddad, I. Khmelnitsky, M. Leucker, D. Neider, R. Roy, and L. Ye, Extracting Context-Free Grammars from Recurrent Neural Networks using Tree-Automata Learning and A-star Search, ICGI’21.
• I. Khmelnitsky, D. Neider, R. Roy, B. Barbot, B. Bollig, A. Finkel, S. Haddad, M. Leucker, and L. Ye, Property-directed verification and robustness certification of recurrent neural networks, ATVA’21.

2020

• A. Finkel, S. Haddad, and I. Khmelnitsky. Minimal coverability tree construction made complete and efficient, FoSSaCS’20
• S. Haddad, and I. Khmelnitsky. Dynamic Recursive Petri Nets, PetriNets’20

2019

• A. Finkel, S. Haddad, and I. Khmelnitsky. Coverability and Termination in Recursive Petri Nets, Petri Nets’19

National Conferences(France):

• Alain Finkel, Serge Haddad et Igor Khmelnitsky. Réification des accélérations pour la construction de Karp et Miller,MSR’19, Angers (in French)

Thesis

• D-collapsibility and its applications. Master thesis, under the supervision of professor R. Meshulam.

Talks

1. Minimal coverability tree construction made complete and efficient - MTV seminar 21.
2. Dynamic Recursive Petri Nets - Video teaser for PetriNet’20.
3. A Tool for the Coverability Problems in Petri Nets - Tool demonstration in MSR’19, Angers France.
4. Coverability and Termination in Recursive Petri Nets - PetriNet’19.

Tools

• MinCov- Python implementation of an algorithm solving the coverability set problem for Petri nets. Based on the work in “Minimal coverability tree construction made complete and efficient”.
• Property directed verification- Implantation of the algorithm developed in “Property-directed verification and robustness certification of recurrent neural networks”.

Teaching

2019-2020

• Architecture and Systems
• Discrete mathematics

2018-2019

• Combinatorial algorithms(in Hebrew)