Neeraj Kumar Singh (HDR)

Neeraj Kumar Singh is an Associate Professor in INPT-ENSEEIHT at the University of Toulouse since 2015. He also holds a joint appointment with the Institute de Recherche en Informatique de Toulouse (IRIT) (UMR CNRS 5505) for conducting the research activities in the ACADIE team.  He leads his research in the area of theory and practice of rigorous software engineering and formal methods to design and implementation of safe, secure and dependable safety-critical cyber-physical systems in the automotive, medical, avionics and nuclear domains. 

In 2024, he was awarded the HDR (Habilitation à diriger des recherches) in Computer Science from INP Toulouse, France, focusing on the development of rigorous safety-critical cyber-physical systems through formal methods. He earned his Ph.D. in Computer Science from INRIA Nancy Grand Est, part of Henri Poincaré University (now known as Université de Lorraine), France, in 2011, where his research centered on the reliability and safety of critical device software systems. This Ph.D. thesis has been published as the book "Using Event-B for Critical Device Software Systems" by Springer.

From 2012 to 2013, he served as a research associate in the Computer Science Department at the University of York, UK, where he contributed to the EPSRC-funded project titled "High-integrity Java Applications using Circus (HiJaC)." From late 2013 until August 2015, he was a research fellow and team leader at the Centre for Software Certification (McSCert) at McMaster University, Canada. During this period, he worked on projects funded by the Ontario Research Fund - Research Excellence (ORF-RE) focused on the certification of safety-critical software-intensive systems, as well as the Automotive Partnership Canada (APC) project on the Network for the Engineering of Complex Software-Intensive Systems (NECSIS) for automotive applications. He earned his master's degree in Optimization System and Security (OSS) from the University of Technology of Troyes, France in 2008. Additionally, he received a Master of Computer Applications (MCA) from Uttar Pradesh Technical University (UTPU), India in 2006 and a Bachelor of Science (B.Sc.) in Computer Science from Lucknow University, India in 2003.

His research focuses on the development and exploration of methodologies for formal engineering processes, including modeling, refinement, simulation, domain knowledge engineering, design automation, and addressing issues related to heterogeneity, composition, safety, and certification in safety-critical cyber-physical systems. He has also proposed a comprehensive development life-cycle along with a suite of techniques and tools for creating highly critical systems. This approach employs formal techniques that span from requirements analysis to automatic source code generation, utilizing multiple intermediate layers and a rigorous safety assessment methodology. His research interests encompass formal modeling, refinement and proofs, meta-modeling, hybrid systems, domain knowledge engineering, cyber-physical systems, formal methods, model checking, automated theorem proving, programming languages, algorithmic synthesis, automatic code generation, verification of medical protocols, software engineering, tabular expressions, software and system certification, assurance cases, model-driven engineering, and biomedical signal processing, including the code generation tool EB2ALL.

He received the Best Paper Awards at 

He has authored more than 95 peer-reviewed research articles published in esteemed journals, books, and international conferences. Furthermore, he is the author of three books. His involvement in scientific activities encompasses roles as a program committee chair, program committee member, journal guest editor, journal reviewer  and external reviewer for ANR (France) and NSERC (Canada) projects. Additionally, he serves as a key project leader and scientific coordinator in various research initiatives centered on formal methods and systems engineering.