Ajay Krishna- Postdoctoral Researcher

Hi! I am currently a Postdoctoral Researcher in the CONVECS team at Inria, Grenoble. My research focuses on formal verification and analysis of industrial IoT applications. I defended my PhD thesis in December 2020. During my thesis, I worked on leveraging formal methods to build behaviourally correct IoT applications. The work was done in collaboration with Nokia Bell Labs under the supervision of Gwen Salaün, Radu Mateescu, and Michel Le Pallec.
I received my Masters degree specializing in High-confidence Embedded and Cyberphysical Systems from Université Grenoble Alpes - ENSIMAG in 2017. Previously, I worked at Thomson Reuters as a Software Engineer contributing to the software applications needed to editorially enhance judicial content (Westlaw®, Findlaw®). I have a Bachelor of Engineering degree in Computer Science from Visvesvaraya Technological University.

Interests

formal methods, verification, internet of things, IIoT, automated verification, business process, software engineering

Research projects

Modelling and Verification for the IoT [code] [video] A formal model of an IoT application was developed from its Web of Things specification. The model was used as the basis for checking for certain quantitative and qualitative properties. The applications needing reconfiguration are checked for the impact of reconfiguration.
Verification of BPMN (VBPMN) [code] Encoding BPMN models as formal models and integrating them to a formal verification toolbox to perform formal analysis using model checking and equivalence checking techniques.

Publications

R-MOZART: A Reconfiguration Tool for WebThings Applications, Companion ICSE'21. Francisco Durán, Ajay Krishna, Michel Le Pallec, Radu Mateescu, Gwen Salaün
Seamless Reconfiguration of Rule-based IoT Applications, SEAMS'21. Francisco Durán, Ajay Krishna, Michel Le Pallec, Radu Mateescu, Gwen Salaün
MOZART: Design and Deployment of Advanced IoT Applications, WWW'20. Ajay Krishna, Michel Le Pallec, Alejandro Martinez, Radu Mateescu, Gwen Salaün
Checking business process evolution, Science of Computer Programming. Ajay Krishna, Pascal Poizat, Gwen Salaün
IoT Composer: Composition and deployment of IoT applications, Companion ICSE'19. Ajay Krishna, Michel Le Pallec, Radu Mateescu, Ludovic Noirie, Gwen Salaün
Rigorous design and deployment of IoT applications, Formalise'19. Ajay Krishna, Michel Le Pallec, Radu Mateescu, Ludovic Noirie, Gwen Salaün
Automated Composition, Analysis and Deployment of IoT Applications, TOOLS'19. Francisco Durán, Gwen Salaün, Ajay Krishna
Automated analysis of industrial workflow-based models, SAC'18. Mario Cortes Cornax, Ajay Krishna, Adrian Mos, Gwen Salaün
VBPMN: Automated Verification of BPMN Processes, IFM'17. Ajay Krishna, Pascal Poizat, Gwen Salaün
Checking Business Process Evolution, FACS'16. Pascal Poizat, Gwen Salaün, Ajay Krishna