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

profile-picture

Hi there!

I am a Senior Research Scientist at IITB Trust Lab, IIT Bombay. My research focuses on the formal verification of reactive systems, in particular, real-time and stochastic systems. To analyze and verify such systems, I have worked on a range of techniques, including model learning, model checking, conformance testing, and runtime verification.
More broadly, my research combines the study of theoretically challenging problems in formal verification with the development of tools that validate and evaluate the resulting techniques.

At IIT Bombay, I work with S Akshay on the verification of stochastic systems and on developing formal guarantees for AI-based models. Previously, I held postdoctoral positions at Université libre de Bruxelles and Inria/IRISA Rennes. At ULB, I worked with Jean-François Raskin on learning models for real-time systems and on controller synthesis for stochastic models such as MDPs and POMDPs. At Inria/IRISA, I worked with Thierry Jéron and Ocan Sankur on conformance testing and runtime verification.

I received my Ph.D. in Computer Science from Chennai Mathematical Institute under the supervision of B Srivathsan and Paul Gastin (LMF, ENS Paris-Saclay). My doctoral research focused on the verification of real-time systems modeled as timed automata.

email: sayan at cse dot iitb dot ac dot in

Education

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

    Employment

    present
  • Senior Research Scientist
    IITB Trust Lab, Department of CSE, IIT Bombay, India
  • 2026
  • Postdoctoral fellow
    DEVINE, Inria/IRISA Rennes, France
  • 2025
  • Postdoctoral fellow
    Université Libre de Bruxelles, Belgium
  • 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. Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning
      Debraj Chakraborty, Anirban Majumdar, Prince Mathew, Sayan Mukherjee, Jean-François Raskin
      to appear in proceedings of   CAV 2026
      [ pre-print | tool ]
    2. 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 ]
    3. 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 ]
    4. 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 ]
    5. 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 ]
    6. 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 ]
    7. 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 ]
    8. 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 ]