A. Selected Industry Sponsored Projects

Domain: Verification of Digital Integrated VLSI Circuits:

1. Intel (Folsom, USA and Haifa, Israel)      2002 - 2005
   Formal methods for verification of architectural properties and computing formal coverage metrics was integrated into Intel’s Formal Verification tool suite developed at Intel, Haifa.
2. National Semiconductors, (Santa Clara, USA)      2003 – 2007
   A tool called GENSTIMULI was developed for the Technology Infrastructure Group of National Semiconductors (now TI), which uses formal methods for generating tests for custom cell characterization.
3. Synopsys, (Bangalore, India and Massachusetts, USA)      2003 – 2007
   Design of Assertion Languages and Formal Specification Formalisms (some of which are now part of the SystemVerilog Standards). Several toolkits and patented verification technologies were developed.
4. Intel (Bangalore, India)      2009 – 2012
   Formal methods for post-silicon validation of bug-fixes and Counter-example Ranking in Intel’s processors. PhD student, Srobona Mitra, won the Google Anita Borg Woman in Engineering Award for this work.
5. Synopsys CAD Laboratory       2009 –
   Synopsys CAD Labs, IIT Kharagpur was set up for undertaking projects in the areas of design automation for verification, testing, and security. Synopsys conferred the prestigious Charles Babbage Grant to this Lab.

Domain: Verification of Mixed-Signal Integrated Circuits:

1. National Semiconductor Corp., (Greenock, Scotland)      2007 - 2010
   Methods for verifying integrated power management units (PMUs) which are large integrated AMS circuits used in portable power devices like cell phones, PDAs and Laptops. The methods use formal hybrid automata based behavioral models.
2. Semiconductor Research Corporation (SRC) (USA)      2008 – Date
   Technology for verification of formal analog properties over AMS simulators. Phase-2 of the project deals with abstract interpretation of formal equivalence features between AMS designs/models.
3. Texas Instruments, (custom funded via Semiconductor Research Corp)      2018 – Date
   Technology for formal coverage management of large analog and mixed-signal integrated circuits.
4. Intel (USA)      2018 – 2021
   Technology for mining dense time assertions from time series data

Domain: Verification of Power Intent and Power Management Strategies

1. Synopsys (California, USA and Bangalore, India)      2008 - 2013
   Formal verification technology for verifying the architectural power management strategy of large integrated circuits. A tool has been developed using the technology.
2. Intel (Bangalore, India)      2010 – 2012
   Tool for evaluating power management strategies for mobile portable platforms.
3. Intel Global Research (USA)      2015 – Date
   Formal verification of power management strategies for mixed-signal power domains.

Domain: Verification of Automotive Control

1. General Motors (India Science Labs)      2007 - 2009
   Technology for verification of formal properties on the fly over execution traces of UML state-charts was integrated into a tool being used by GM for verification of automotive control software.
2. General Motors (India and Warren, USA)      2009 – 2012
   Formal verification of feature specifications for automotive control subsystems using AI planning techniques. This research led to a joint patent with General Motors.

Domain: Software Verification

1. Google       2008 - 2009
   Developing formal methods for verifying web-service protocols.
2. Hindustan Aeronautics Ltd.       2015 – 2018
   Formal verification of India’s first indigenous avionic Real Time Operating System. The RTOS is now flying with the Hawkeye aircraft of HAL.

Domain: Verification of Railway Signaling and Interlocking

1. Indian Railways       2013 - 2017
   Formal methods for proving the correctness of Electronic Interlocking Logic for railway signaling.

B. Selected Government Sponsored Projects

1. Developing Explainable Artificial Intelligence for Connected and Autonomous Vehicles  (2019 - 2021)
   DST-UKIERI project in collaboration with the Warwick Manufacturing Group, UK. This project aims to develop explainable and safe reinforcement learning frameworks for autonomous driving and ADAS tasks.
2. Artificial Intelligence For Societal Needs  (2013 - 2017)
   This project funded under the Diamond Jubilee Research Grant, IIT Kharagpur brought together researchers from various departments to work for AI solutions to problems in Agriculture, Environment, Power, Disaster Management and Urban Planning.
3. FMSAFE: A Networked Centre for Formal Methods for Safety Critical Systems  (2017 - 2020)
   This IMPRINT project funded by MHRD and Ministry of Railways, brings together experts from IIT Kharagpur, IIT Bombay and IIT Kanpur to develop formal verification technology for safety critical systems.
4. Decoding And Exploring Ancient Classification of Ragas In Indian Classical Music  (2014 - 2018)
   This project was funded by MHRD under the Science and Heritage Initiative (SandHI). Collaboration with Indian Classical musicians in studying the deep structure of Indian Ragas.
5. AUTOSAFE: Architecture- Aware Timing Analysis And Formal Verification of Automotive Control Systems  (2012 - 2015)
   This project was funded by the Indo-German Science and Technology Center to IIT Kharagpur and TU Munich. This project laid the foundations for the two universities to come together to set up an Indo-German Center for Intelligent Transportation Systems at IIT Kharagpur recently