Home / Projects

Ongoing Projects

"If you keep proving stuff that others have done, getting confidence, increasing the complexities of your solutions - for the fun of it -
then one day you'll turn around and discover that nobody actually did that one! And that's the way to become a computer scientist."
    – Richard Feynman

An Integrated Hierarchical Debugging Framework for XLS Tool-suite

Sponsoring Agency:   Google Inc. (Silicon Research Program)
Duration:   October 2024 – Present
Investigator:   Dr. Aritra Hazra (CSE, IIT Kharagpur)

Integrating Verification and Coverage Management Framework with XLS Tool-suite

Sponsoring Agency:   Google Inc. (Silicon Research Program)
Duration:   November 2023 – Present
Investigator:   Dr. Aritra Hazra (CSE, IIT Kharagpur)

Automation and Setting Up of a Reference Lab for Validating Cryptographic Algorithms/Modules as per ISO/IEC Standards.

Sponsoring Agency:   Ministry of Electronics and Information Technology, Government of India
Duration:   January 2025 – Present
Investigators:   Dr. Abey Jacob, Mr. Raghevendra S Patil, Ms. Smitha Gururaj Havanur and Mr. Annarao Kulkarni (CDAC-Bangalore); Dr. Chester Rebeiro (CSE, IIT Madras); Dr. Aritra Hazra (CSE, IIT Kharagpur); and Ms. A Suganya (SETS-Chennai)

Scalable Formal Property Verification leveraging Property Grouping and Ordering.

Sponsoring Agency:   Synopsys Inc. (USA)
Duration:   August 2021 – Present
Investigators:   Prof. Pallab Dasgupta and Dr. Aritra Hazra (CSE, IIT Kharagpur)
Collaborators:   Trinanjan Chatterjee, Sudipta Kundu and Himanshu Jain (Synopsys, USA)

ML and RL based Predictive Modeling Tool for Spatio-Temporal Temperature map on a Multi-core CPU under Dynamic Workloads

Sponsoring Agency:   Google Inc. (AI/ML Research Program)
Duration:   November 2024 – Present
Investigators:   Prof. Anandaroop Bhattacharya (ME, IIT Kharagpur), Prof. Partha Pratim Chakrabarti and Dr. Aritra Hazra (CSE, IIT Kharagpur)

Information Security Education and Awareness (ISEA) Project Phase III

Sponsoring Agency:   Ministry of Electronics and Information Technology, Government of India
Duration:   July 2024 – Present
Investigators:   Prof. Debdeep Mukhopadhyay, Dr. Sarani Bhattacharya and Dr. Aritra Hazra (CSE, IIT Kharagpur)

Exploring Human and Machine Cognition: Building a Learning Analytics Portal of AI Assisted Problem Solving Models for Visuo-Spatial Tasks

Sponsoring Agency:   Department of Science and Technology (DST), Government of India
Duration:   May 2023 – Present
Investigators:   Dr. Rajlakshmi Guha (RCESH, IIT Kharagpur), Dr. Aritra Hazra and Prof. Partha Pratim Chakrabarti (CSE, IIT Kharagpur)

Formal Methods for Verification of Power Management in Mixed-Signal Designs.

Sponsoring Agency:   Intel, USA
Duration:   September 2015 – Present
Investigators:   Prof. Pallab Dasgupta, Prof. Partha Pratim Chakrabarti and Dr. Aritra Hazra (CSE, IIT Kharagpur)
Collaborators:   Dr. Chunduri Rama Mohan, Rohini Krishnan, Sanjib Basu, Bhushan G. Naware (Intel, India/USA)

Completed Projects

"Practice makes perfect. After a long time of practicing, our work will become natural, skillfull, swift, and steady."    – Bruce Lee

Formal Methods for Verification and Synthesis of Secure Designs.

Sponsoring Agency:   Institute Scheme for Innovative R&D (ISIRD), SRIC, IIT Kharagpur
Duration:   September 2018 – September 2021
Investigator:   Dr. Aritra Hazra (CSE, IIT Kharagpur)

A Framework for Automatic Detection of Fault Attack Vulnerabilities.

Sponsoring Agency:   Cisco University Research Program Fund (A corporate advised fund of Silicon Valley Community Foundation)
Duration:   February 2018 – May 2022
Investigators:   [USA-Team] Prof. Swarup Bhunia, Prof. Mark Tehranipoor ( University of Florida) and [India-Team] Dr. Aritra Hazra (CSE, IIT Kharagpur), Dr. Chester Rebeiro (CSE, IIT Madras)
Collaborators:   Julie McDermott and Misti M. Sangani (Silicon Valley Community Foundation)

Formal Verification and Synthesis of Secure Designs.

Sponsoring Agency:   New Faculty Seed Grant by IC & SR, IIT Madras
Duration:   December 2015 – July 2017
Investigator:   Dr. Aritra Hazra (CSE, IIT Madras)

Formal Methods for Reliable Safety-Critical System Design.

Sponsoring Agency:   New Faculty Initiation Grant by IC & SR, IIT Madras
Duration:   August 2015 – July 2017
Investigator:   Dr. Aritra Hazra (CSE, IIT Madras)

Machine Learning at the Digital-Analog Boundary – A Contract Assurance Framework based on AMS Assertions.

Sponsoring Agency:   Intel, USA
Duration:   September 2018 – August 2024
Investigators:   Prof. Pallab Dasgupta and Dr. Aritra Hazra (CSE, IIT Kharagpur)
Collaborators:   Dr. Chunduri Rama Mohan, Rohini Krishnan, Sanjib Basu, Bhushan G. Naware (Intel, India/USA)

A Formal Coverage Management Framework for AMS Design Verification.

Sponsoring Agency:   Texas Instruments (TI), Semiconductor Research Corporation (SRC)
Duration:   September 2018 – January 2024
Investigators:   Prof. Pallab Dasgupta and Dr. Aritra Hazra (CSE, IIT Kharagpur)
Collaborators:   Scott Morrison, Sudhakar Surendran,Lakshmanan Balasubramanian, Rubin Parekhji (TI, USA) and Leslie Faiers (SRC)

Developing Explainable Artificial Intelligence for Safety Arguments for Connected and Autonomous Vehicles.

Sponsoring Agency:   Department of Science and Technology (DST)UK-India Education and Research Initiative (UKIERI)
Duration:   July 2019 – December 2021
Investigators:   [India-Team] Prof. Pallab Dasgupta, Dr. Aritra Hazra (CSE, IIT Kharagpur) and [UK-Team] Dr. Siddartha Khastgir, Prof. Giovanni Montana, Prof. Paul Jennings (WMG, University of Warwick)

AWS-NAIRP: Creating a Collateral for Supporting Popular ML Applications on AWS Infrastructure through National AI Resource Platform.

Sponsoring Agency:   Amazon Web Services Inc. (Seattle, US)
Duration:   April 2019 – August 2022
Investigators:   Prof. Partha Pratim Chakrabarti, Dr. Abir Das, Prof. Sudeshna Sarkar, Dr. Aritra Hazra, Prof. Pabitra Mitra (CSE, IIT Kharagpur); Dr. Jiaul Hoque Paik, Dr. Plaban Kumar Bhowmick (CET, IIT Kharagpur) and Dr. Debdoot Sheet (EE, IIT Kharagpur)

Developing A Computing and Storage Framework around National Digital Library of India (NDLI) Resources.

Sponsoring Agency:   NMEICT (Ministry of Human Resource Development, Government of India)
Duration:   August 2018 – February 2020
Investigators:   Prof. Sudeshna Sarkar (CAI, IIT Kharagpur), Dr. Aritra Hazra (CSE, IIT Kharagpur), Dr. Arijit Mondal (CSE, IIT Patna), Dr. Ansuman Banerjee (ACMU, ISI Kolkata) and Dr. Nilanjan Banerjee (Onometra Technologies Pvt. Ltd.)
Collaborators:   Prof. Partha Pratim Das (CSE, IIT Kharagpur)

Secure Resource-constrained Communication Framework for Tactical Networks using Physically Unclonable Functions (SeRFPUF).

Sponsoring Agency:   DFTM-DRDO, Bangalore
Duration:   November 2017 – December 2023
Investigators:   Prof. Debdeep Mukhopadhyay, Dr. Rajat Subhra Chakraborty and Dr. Aritra Hazra (CSE, IIT Kharagpur)

FMSAFE: A Networked Centre for Formal Methods in Validation and Certification Procedures for Safety – Critical ICT Systems at IIT Kharagpur.

Sponsoring Agency:   Ministry of Human Resource Development, Department of Higher Education, Government of India; Ministry of Railways, Rail Bhavan, New Delhi (India)
Duration:   February 2017 – May 2023
Investigators:   Prof. Pallab Dasgupta, Prof. Partha Pratim Chakrabarti, Dr. Soumyajit Dey and Dr. Aritra Hazra (CSE, IIT Kharagpur)
Collaborators:   Prof. Supratik Chakraborty (CSE, IIT-Bombay);   Prof. Sandeep Shukla and Dr. Indranil Saha (CSE, IIT-Kanpur)

A Formally Verified Multi-precision Arithmetic Library for Cryptographic Applications.

Sponsoring Agency:   CAIR-DRDO, Bangalore and IC & SR, IIT Madras
Duration:   September 2015 – September 2017
Investigators:   Dr. Chester Rebeiro, Prof. V. Kamakoti and Dr. Aritra Hazra (CSE, IIT Madras)
Collaborator:   Lexy Alexander (CAIR-DRDO, Bangalore)

Projects Completed as Research Consultant

"You can't plant a seed without getting your hands dirty."    – Mariah Dillard

AUTOSAFE: Architecture-aware Timing Analysis and Optimization of Safety-Critical Automotive Software.


Sponsoring Agency:   Indo-German Science and Technology Centre (IGSTC)
Duration:   April 2012 – December 2014
Investigators:   Prof. Partha Pratim Chakrabarti and Prof. Pallab Dasgupta (CSE, IIT Kharagpur)
Collaborators:   Prof. Samarjit Chakraborty (TU Munich, Germany), Karsten Albers (INCHRON GmbH, Germany), Arun Bahulkar and R. Venkatesh (TRDDC Pune, India)

Building Reliable Embedded Real-Time Systems: An Approach Combining Formal Methods and Testing.


Sponsoring Agency:   DST Indo-Brazil
Duration:   February 2011 – July 2014
Investigators:   Prof. Partha Pratim Chakrabarti and Prof. Pallab Dasgupta (CSE, IIT Kharagpur)
Collaborators:   Augusto Sampaio (Federal University of Pernambuco, Brazil) and Jose Carlos Maldonado (USP (Sao Paolo University), Brazil)

Power Intent Verification for Multi-Voltage Low Power Designs.


Sponsoring Agency:   Synopsys, India/USA
Duration:   August 2009 – June 2011
Investigators:   Prof. Pallab Dasgupta and Prof. Ajit Pal (CSE, IIT Kharagpur)
Collaborators:   Manish Pandey, Kevin Harer (Synopsys, USA), Praveen Tiwari, Puneet Jethalia and Trinanjan Chatterjee (Synopsys, Bangalore, India)

Platform Architecture Modeling for Exploring SOC Power Management Policies.


Sponsoring Agency:   Intel, India
Duration:   August 2010 ― July 2011
Investigators:   Prof. Pallab Dasgupta and Prof. Chitta Ranjan Mandal (CSE, IIT Kharagpur)
Collaborators:   Dr. Krishna Paul (Intel, Bangalore, India)

Coverage Metrics for Design Intent Coverage.


Sponsoring Agency:   Intel, USA
Duration:   August 2006 ― July 2009
Investigators:   Prof. Pallab Dasgupta and Prof. Partha Pratim Chakrabarti (CSE, IIT Kharagpur)
Collaborators:   Dr. Chunduri Rama Mohan (Intel, Folsom, USA)

Modification of Gunfinder-Studio Software


BE Final Year Project
Duration: June 2005 – May 2006
Supervisor:   Prof. Chandan Majumdar (CSE, Jadavpur University)

Prototype Tools Developed

"For a successful technology, reality must take precedence over public relations, for Nature cannot be fooled."    – Richard Feynman

PARLE-G : A CAD Tool for Automated Assessment of Provable Learnability from PUF Representations.


Summary:   This tool analyzes the PAC-learnability of PUF designs from an architectural level. To enable this, we propose a formal PUF representation language (PUF-G) by which any architectural PUF design and its compositions can be specified upfront. This PUF specification can be automatically analyzed through this tool by translating the same to an interim model and finally deriving the PAC-learnability bounds from the model. Such a tool will help the designer to explore various compositional architectures of PUFs and its resilience to ML attacks automatically before converging on a strong PUF design for implementation.
Status:   Completed – Developed as a part of a DRDO Project

CoveRT : A Coverage Reporting Tool for Analog Mixed-Signal Designs.


Summary:   This tool is built around a library of standard AMS coverage primitives and a language for defining coverage bins around these primitives. It collects the coverage information by interfacing with standard commercial simulators and save these across simulation runs. The tool can work online with commercial simulators while the simulation executes, or offline by replaying the waveforms collected during simulation.
Status:   Completed – Delivered to TI (USA) as part of SRC project for Testing & Development

Fault-Droid : A Tool for Analyzing Information Leakage of Block Ciphers through Fault Attacks.


Summary:   This tool automatically analyze the vulnerability with respect to fault attacks. It explores the entire fault attack space; identifies the single/multiple fault scenarios that can be exploited by a differential fault attack (DFA); rank-orders them with respect to criticality; and provides design guidance to mitigate the vulnerabilities at low cost. Fault-Droid uses a formal model of fault attacks on a high-level specification of a block cipher and hence is equally applicable to both software and hardware implementation of the cipher.
Status:   Completed – Developed as part of a CISCO University Research Grant Project

Power-Trams : A Tool for Formal Verification and Coverage Analysis of Mixed-Signal Power Management.


Summary:   This tool extracts analog features with latencies and leverage annotated UPF specifications to generate formal properties in order to validate the mixed-signal power management logic. The properties are generated considering the power management for both the analog as well as digital power domains. It also provides a formal analog assertion template where analog domain experts can fill in analog behaviors with their built-in domain knowledge, so that formal properties are gleaned out and used in verification. Further, it supports a framework for formal coverage analysis of PML leveraging auxiliary power machine, thereby providing a comprehensive verification as well as coverage analysis flow.
Status:   Completed – Delivered to Intel Inc. (USA) for Testing

Power-Tructor : A Tool for Formal Verification and Coverage of Architectural Power Intent.


Summary:   This tool extracts per-domain assertions (in SVA) from UPF-specifications and leverage these synthesized assertions to formulate the architectural power intent properties. Finally, this tool invokes Magellan tool (of Synopsys) to formally verify those generated assertions over the power control logic of a design. Moreover, this tool is also capable of analyzing the global power state coverage of the power management logic. Interestingly, the tool can handle the power management strategy implemented partially in hardware and partially in software/firmware.
Status:   Completed – Delivered to Synopsys Inc. (USA) for Productization

SoC-Residency-Simulator : A Power-Performance Evaluator for Given Workloads


Summary:   This tool is built on top of some existing SystemVerilog simulator. The tool takes as input a given partition of the SoC components into power domains and a software strategy for deciding the residencies. It runs on various workloads to analyze the performance of the integrated power management and produce a report on the power consumption/wastage of each components of the design. This solution will also help to re-organize the components and power domains of a design to get better power utilization profile.
Status:   Completed – Delivered to Intel Corp. (India) for In-house Experiments

CovAnalyzer : A Completeness Checker for Design Specifications


Summary:   This tool analyzes the completeness of a formal specification against a given fault model. Current tool considers single stuck-at-fault on the interface signals as the fault model and supports specifications written in various temporal languages like LTL, ForSpec (of Intel Corp.) or SVA.
Status:   Completed – Delivered to Intel Corp. (USA) for Productization