Sayan Mukherjee | সায়ন মুখার্জী

profile-picture
email: sayan dot mukherjee at irisa dot fr

Hi there!

I am a CNRS post-doctoral researcher with Thierry Jéron in the DEVINE group at IRISA/Inria Rennes. My primary research is in formal verification of reactive systems, in particular, real-time systems and stochastic systems. Currently, we are working on efficient test synthesis techniques for real-time systems. We are also exploring runtime verification techniques for infinite duration timed and untimed specifications.

Before coming to Rennes, I was a post-doctoral fellow with Jean-François Raskin in the Formal Methods and Verification group at Université Libre de Bruxelles. We worked on learning models for real-time systems. Alongside, I also got introduced to the area of verification of stochastic systems modelled as MDPs and POMDPs. We work on the controller synthesis problem for such models.

I did my Ph.D. in Computer Science from Chennai Mathematical Institute under the supervisions of B Srivathsan (Chennai Mathematical Institute) and Paul Gastin (LSV, ENS Paris-Saclay). During this time, I worked on verification of real-time systems that are modeled using Timed Automata.

Education

2022
  • Ph.D. in Computer Science
    Advisors: Prof. Paul Gastin and Prof. B Srivathsan
    Chennai Mathematical Institute
    • 2016
  • M.Sc. in Applications of Mathematics
    Chennai Mathematical Institute
    • 2014
  • B.Sc. in Mathematics
    St. Xavier's College (Autonomous), Kolkata
    • 2011

    Employment

    present
  • Postdoctoral fellow
    Advisor: Prof. Thierry Jéron
    DEVINE, IRISA / Inria Rennes
    • February, 2025

    December, 2024
  • Postdoctoral fellow
    Advisor: Prof. Jean-François Raskin
    Université Libre de Bruxelles
    • April, 2022

    During May - July, 2015, I did a summer internship with Prof. Subhas Chandra Nandy, working on a problem in Computational geometry, at Indian Statistical Institute, Kolkata.

    Academic Service

    Publications

    1. Prompt Runtime Enforcement
      Ayush Anand, Loïc Germerie Guizouarn, Thierry Jéron, Sayan Mukherjee, Srinivas Pinisetty, Ocan Sankur
      in proceedings of   ATVA 2025, LNCS 16145, 135 -- 156, Springer
      [ pre-print | conference version | doi: 10.1007/978-3-032-08707-2_7 ]
    2. Learning Event-recording Automata Passively
      Anirban Majumdar, Sayan Mukherjee, Jean-François Raskin
      in proceedings of   ATVA 2025, LNCS 16145, 27 -- 48, Springer
      [ pre-print | conference version | doi: 10.1007/978-3-032-08707-2_2 | tool ]
    3. Greybox Learning of Languages Recognizable by Event-Recording Automata
      Anirban Majumdar, Sayan Mukherjee, Jean-François Raskin
      in proceedings of   ATVA 2024, LNCS 15054, 235 -- 256, Springer
      [ pre-print | conference version | doi: 10.1007/978-3-031-78709-6_12 | tool ]
    4. Bi-Objective Lexicographic Optimization in Markov Decision Processes with Related Objectives
      Damien Busatto-Gaston, Debraj Chakraborty, Anirban Majumdar, Sayan Mukherjee, Guillermo A. Pérez, Jean-François Raskin
      in proceedings of   ATVA 2023, LNCS 14215, 203 -- 223, Springer
      [ pre-print | conference version | doi: 10.1007/978-3-031-45329-8_10 ]
    5. Reachability for Updatable Timed Automata Made Faster and More Effective
      Paul Gastin, Sayan Mukherjee, B Srivathsan
      in proceedings of   FSTTCS 2020, LIPIcs 182, 47:1 -- 47:17, Schloss Dagstuhl--Leibniz-Zentrum für Informatik
      [ pre-print | conference version | video | doi: 10.4230/LIPIcs.FSTTCS.2020.47 ]
    6. Fast Algorithms for Handling Diagonal Constraints in Timed Automata
      Paul Gastin, Sayan Mukherjee, B Srivathsan
      in proceedings of   CAV 2019, LNCS 11561, 41 -- 59, Springer
      [ pre-print | conference version | doi: 10.1007/978-3-030-25540-4_3 ]
    7. Reachability in Timed Automata with Diagonal Constraints
      Paul Gastin, Sayan Mukherjee, B Srivathsan
      in proceedings of   CONCUR 2018, LIPIcs 118, 28:1 -- 28:17, Schloss Dagstuhl--Leibniz-Zentrum für Informatik
      [ pre-print | conference version | doi: 10.4230/LIPIcs.CONCUR.2018.28 ]