Short-term visitors


Vaishnavi Sundararajan (PhD CMI 2018, post-doc at IRISA) visited LaBRI March 19th to 22nd, 2019. She gave a talk at the Méthodes Formelles seminar on the certification of security protocols (more specifically: on a theory of assertions for Dolev-Yao models), and she participated in a meeting of  the ANR project BRAVAS on vector addition systems.

Jayakrishnan M. (PhD student, IMSc, Chennai) is visiting LIRMM from March 16th to May 31st, 2019. He will work with Christophe Paul on parametrized algorithms for partitioning problems in directed graphs.

Alain Finkel (LSV) visited IIT Bombay February 13 to March 11, 2019, to work again with S. Akshay and S. Krishna. They continued their discussion on VASS extended with three unbounded and on recent FIFO models.

Philippe Schnoebelen (LSV) visited CMI from January 17th to January 31st, 2019. He worked with Ramanathan S. Thinniyam (a postdoctoral researcher at CMI) on algorithmic questions for piecewise testable languages, focusing on the equivalence classes of Simon’s subword congruence. This is part of a general research agenda (see [Karandikar, Schnoebelen. The height of piecewise-testable languages and the complexity of the logic of subwordsLogical Methods in Computer Science, to appear]) aiming at understanding the piecewise complexity of various languages and constructions.

Pascal Weil visited CMI from January 15th to January 26th, 2019. He worked with Madhavan Mukund on the functioning of UMI ReLaX.

Alain Finkel (LSV) visited CMI from January 11th to February 12th, 2019. He worked with M. Praveen on FIFO systems.


Vincent Penelle (LaBRI) visited IIT Goa from December 17th to 21st 2018, to work with Sreejith A.V. They continued the work initiated with Gabriele Puppis on transducers on words over linear countable ordering. They also worked on the links between certain pumping lemmas for a language class and effective computation of downward and upward closure of languages from that class. From that, they hope to obtain complexity result for the computation of downward closure of languages of one-counter automata and image languages of sweeping transducers. Both projects are ongoing. The second one will involve Prince, a Junior Research Fellow at IIT Goa, soon to be a PhD student of Sreejith.

Alain Finkel (LSV) visited IIT Bombay December 3 to 9, 2018, to work with S. Akshay and S. Krishna. They discussed extended VASS with three unbounded counters and tried to solve some open problems.

Pascal Weil (LaBRI) visited CMI October 22nd to November 3rd, 2018. He worked with B. Srivathsan and Madhavan Mukund on the preparation of the workshop CAALM (January 2019) and he hosted, with Madhavan Mukund, the AURA meeting.

Ramanathan S. Thinniyam (PhD student, IMSc, Chennai) visited LSV from August 19th to 26th, 2018. He worked with Philippe Schnoebelen on combinatorial aspects of embedding relations. In particular, there is a rich theory for embeddings between words or strings that could be leveraged when  considering embeddings between trees or graphs.

Sreejith A.V. (IIT Goa) visited LaBRI from September 26th to October 4th 2018, to work with Vincent Penelle. They held exploratory discussions on probabilistic algorithm for counting problems. They also started to define transducers over words on linear countable ordering, and study the equivalence and origin-equivalence problem on this model together with Gabriele Puppis, this last work being currently in progress.
Sreejith also gave a seminar on Languages over countable linear orderings and had discussions with Mohamed Mosbah about potential student exchanges between IIT Goa and Bordeaux INP.

S. Akshay (IIT Bombay) visited LSV from July 3rd to 13th. He worked with Paul Gastin on timed extensions of multithreaded recursive programs. Together with Sparsa Roy Choudhurry (PhD student at IITB) and S. Krishna (IITB), he is developing a tool to check non-emptiness of such systems under scope bounded restriction. Their approach via tree-width actually covers a much larger under-approximation than scope-bounded. They have obtained a mature theory for this timed extension and are actively developing a prototype tool.

K. Narayan Kumar (CMI) visited LaBRI June 17 to 24 to hold discussions with Pascal Weil. He also gave a seminar titled Verification of Asynchronous Programs with Locks. He then visited LSV June 25 to July 1st, to work with Benedikt Bollig, Marie Fortin and Paul Gastin on temporal logics for message sequence charts (MSCs). As a consequence of results obtained by Bollig, Fortin and Gastin which will appear in CONCUR’18, they obtained a two-dimensional temporal logic which is expressively complete for the first-order logic over MSCs. Their goal is to find a one-dimensional temporal logic which is also FO-complete. They proved that this is possible when restricting to bounded MSCs. They are currently investigating the unbounded case.

S. Krishna (IIT Bombay) visited LSV from June 3rd to 16th. She worked with Paul Gastin on an unambiguous version of the famous factorization forest theorem due to Imre Simon. They proved that, given a morphism to a finite semigroup, one can construct an unambiguous automaton with some nice properties. Then, applying a refined version of state elimination, one obtains an unambiguous regular expression such that each sub-expression E is mapped to a single semigroup element, which is moreover an idempotent if E^+ or E^ω is also a sub-expression. The construction works for both finite and infinite words. An article is in preparation.
The work on regular transducer expressions which appeared in LICS’18 is based on this unambiguous factorization forest.

B. Srivathsan (CMI) visited LaBRI  June 1st to 29. He worked with Frédéric Herbreteau and Igor Walukiewicz on partial-order techniques for timed automata. Together with Govind Rajanbabu (co-tutelle Ph.D. student LaBRI/CMI), they develop new abstraction techniques for timed automata that take concurrency into account to improve verification algorithms. An article based on this work is in preparation. They are also working on improving their abstraction techniques by using partial order techniques.

Madhavan Mukund (CMI) visited LaBRI during May 14-25, 2018.  He and Anca Muscholl (LaBRI) are jointly supervising the PhD thesis of Adwitee Roy, who was also visiting LaBRI during the summer of 2018. During this visit, some work was initiated in the area of synthesizing distributed negotiations from sequential specifications.
Madhavan Mukund then visited IRIF from May 28 to June 8 to work with Ahmed Bouajjani and Constantin Enea. This visit was part of the CEFIPRA project AVeCSo. Research discussions were on two ongoing topics:  formalizing replicated data types that support multiple levels of consistency (joint work with Gautham Shenoy R. and S. P. Suresh, CMI) and verification techniques for formal models of web services (joint work with Nisarg Patel, M.Sc. student at CMI who was an intern at IRIF in May 2017).

M. Praveen visited LSV May 11 to 24. He continued the work with Alain Finkel on flat FIFO systems, initiated when Alain Finkel visited CMI in February 2018. Archit, the MSc student at CMI involved in this work, finished his MSc thesis based on a part of this work. M. Praveen also worked with Philippe Schnoebelen at LSV on characterizing functions which are weakly computable by grammar controlled vector addition systems, preparing a future submission.

B. Srivathsan visited LSV between May 2 – 18, and PhD student Sayan Mukherjee visited LSV between May 2 – 31, to work with Paul Gastin on simulation relations for timed automata with diagonal constraints. During this visit, they worked on a better formulation of their previous work on such a simulation relation, and extended it to a larger class of automata. Better algorithms for simulation tests between zones were discussed. An extended journal version of their preliminary results is in preparation.

Alain Finkel visited CMI January 30 to February 18, to work with M. Praveen and a M.Sc. student, Archit, on flat FIFO systems. He also participated in the Future Tour (February 1-2). He then traveled to IISc Bangalore, CSA Department February 19 to 23, to work with Deepak D’Sousa, K.V. Raghavan and Sriram Rajamani (the latter, Director of Microsoft India). They discussed the verification of concurrent programs and he gave two seminars at Bangalore on WSTS. Alain Finkel then proceeded to the CSE Department, IIT Bombay February 23 to March 12, to work with S. Akshay. He gave two lectures on WBTS and the famous Erdös-Tarski Theorem and a seminar on WSTS for the faculty members. He also was invited on February 28 by the research group on the verification of programs in Pune, and at the TCS Department, TIFR by Paritosh K. Pandya. He visited also the Homi Bhabha Centre for Science Education, Tata Institute of Fundamental Research, to share his research on the pedagogics of mathematics. Finally, he participated in the ENS Paris-Saclay delegation which visited the IITB on March 7.

Pascal Weil (LaBRI) visited CMI January 27 to February 2, 2018. He worked with Paul Gastin (LSV), Madhavan Mukund and K. Narayan Kumar on the organization of the future ReLaX events. He also participated in the Bonjour India event sponsored by Institut Français India. The previous week, he taught a class at the Mathematics Department of the University of Kerala at Kariavattom, under the Government of Kerala’s Erudite Program.

Xavier Goaoc (Université Paris Est) visited CMI from January 20 to 27, 2018. He worked with Priyavrat Deshpande  on the organization of student exchanges between CMI and Université Paris Est, and gave three lectures, one of which was within a Computational Geometry Day at CMI, organized by Priyavrat Deshpande. He also initiated discussions with Samir Datta on algorithmic questions on geometric graphs, with M. Praveen on the geometric questions underlying some questions in verification, and with Priyavrat Deshpande on notions of topological complexity.

Shweta Bhandari (PhD student at MNIT Jaipur) visited LaBRI January 15 to 31, 2018. She worked with Akka Zemmari (LaBRI) on the use of typical paths and machine learning techniques to detect malware apps. They also worked (with Frédéric Herbreteau, LaBRI) on the use of model checking to detect data leakage in colluding apps.

Vineeta Jain (PhD student at MNIT Jaipur) visited LaBRI January 15 to 31, 2018. She worked with Mohamed Mosbah (LaBRI) on device-to-device attacks in Android, mainly focussed on attacks launched through evil twins in the network.

Paul Gastin (LSV) visited CMI January 10 to February 14. He worked with K. Narayan Kumar on the separation problem for first-order logic over message sequence charts (MSCs) which are behaviors of finite state distributed systems communicating via unbounded FIFO channels. They proved that in general first-order logic is not separable over MSCs. This negative result holds even for existentially bounded MSCs. In contrast, for universally bounded MSCs, they gave an inductive construction showing that FO is separable. During this visit, Paul Gastin also worked on timed systems with B. Srivathsan and Sayan Mukherjee (a jointly advised PhD student, more details here). They developed a symbolic reachability analysis for timed systems featuring diagonal constraints. The main difficulty is to extend the zone based approach to cope with diagonal constraints and in particular to check zone inclusion up to a simulation relation. This work resulted in a paper accepted at CONCUR’18.


Pascal Weil (LaBRI) visited CMI November 11 to 18, 2017, on the occasion of the formal signing of UMI ReLaX. He worked with Madhavan Mukund on the planification of the UMI’s activities.

Paul Gastin (LSV) visited IIT Bombay October 30 to December 23, 2017. He worked on combinator expressions with S. Krishna and Vrunda Dave (PhD student at IITB), and on timed systems with S. Akshay, S. Krishna and Sparsa Roy Choudhury (PhD student at IITB). More…

K. Narayan Kumar (CMI) visited LSV and IRIF June 25 to July 9 and again, July 16 to 22, 2017. He worked with Paul Gastin, revisiting the classical problems of expressive completeness and separation theorems for logics over words and Mazurkiewicz traces, with a view to extending these results to other partially ordered structures. He worked also with Ahmed Bouajjani and with M.F Atig (Uppsala Univ.) and P. Saivasan (Univ. Braunschweig) on the analysis of asynchronous programs with lock based  synchronization.

S. Krishna (IIT Bombay) visited LSV June 29 to July 13, 2017. She worked with Paul Gastin on the analysis of timed systems, and with Patricia Bouyer-Decitre on stochastic timed games. Her visit was partially supported by Project AVeRTS. More…

S. Akshay (IIT Bombay) visited LSV June 26 to July 17, 2017. He worked with Paul Gastin, S. Krishna and others on the analysis of timed systems. His visit was partially supported by Project AVeRTS. More…

M. Praveen (CMI) visited LSV June 18 to July 1, 2017. He worked with Philippe Schnoebelen on characterizing functions weakly computable by grammar controlled vector addition systems, concentrating on proving that hyper-Ackermannian functions can be weakly computed. He also worked with Stéphane Demri on satisfiability of constraint LTL over ordered domains, concentrating on identifying problems that they can collaborate on in the coming months. He also worked with Alain Finkel, identifying potential topics for MSc thesis. The topics discussed consist of flattable FIFO systems and approaches for implementation of verification algorithms for counter systems.

C. Aiswarya (CMI) visited LSV June 1st to 25, 2017. She worked with Paul Gastin and Benedikt Bollig, on propositional dynamic logic on data words over an ordered domain, concentrating on questions of expressiveness and on the complexity of satisfiability.

Amaldev Manuel (CMI) visited LSV and IRIF May 19th to June 30th 2017. He worked with Paul GastinStefan Göller and Thomas Colcombet on problems related to logic, games and regular languages. More…

Madhavan Mukund (CMI) visited LSV and IRIF May 13 to 26 2017. He participated in the 20th anniversary celebration of LSV and worked with Ahmed Bouajjani and Constantin Enea on formal models for session systems and new consistency notions for replicated data.

Antoine Meyer (LIGM) visited IMSc April 1st to April 11, 2017. He worked with Kamal Lodaya on augmentations of temporal logic, such as counting and graded temporal logic. More…

Didier Caucal (LIGM) visited IMSc April 1st to 22, 2017. He worked with Kamal Lodaya on monadic second-order decidability on the event structures of one safe Petri nets. They considered a property more general than that of the existence of a grid which had been considered by Thiagarajan. The restriction to the existence of a grid for the undecidability of the monadic theory remains to be established.

Philippe Schnoebelen (LSV) visited CMI January 4 to February 7 and February 18 to March 5, 2017. He gave  a series of lectures on Algorithmic Aspects of WQO Theory and worked with M. Praveen (CMI) on grammar controlled vector addition systems, and with K. Narayan Kumar (CMI) on ideal-based data structures and algorithms for WQOs.

Paul Gastin (LSV) visited CMI January 1st to March 10, 2017.  He worked with C. Aiswarya (CMI) on distributed control for asynchronous systems with Rendez-vous communication and on formal methods for the verification of distributed algorithms; with B. Srivathsan (CMI) on parity games; with Amaldev Manuel (CMI) and Govind (CMI Master student) on automata and logical characterizations of regular languages of undirected words. The specifications in logics (FO, MSO, …) use non-oriented predicates (e.g., neighbor instead of successor). The corresponding languages are closed under reverse. The goal is to find algebraic characterizations for such reversible regular languages.

Ahmed Bouajjani (IRIF) visited CMI January to February, 2017.

Alain Finkel (LSV) visited CMI January 17 to February 6, 2017. He worked on counter systems with M. Praveen and gave two seminar on Well Structured Transition Systems.