Home / Research

Research Areas

"Imagination is more important than knowledge. For knowledge is limited to all we know and understand,
while imagination embraces the entire world, and all there ever will be to know and understand."    – Albert Einstein

Formal methods specify rigorous theoretical and mathematical models to design software and hardware systems and use mathematical proofs to formally validate and certify the design behaviors, ensuring its correctness, power management, reliability, security, quality and robustness attributes.
VLSI designs and integrated circuits are manufactured using several computer-aided design (CAD) frameworks where many challenging algorithmic problems need to be solved, including design synthesis, floor-planning, placement and routing, to deliver a final chip. Additionally, to ensure the correctness during various phases of the chip design, a gamut of simulation, formal and semi-formal techniques are applied both in pre-silicon as well as post-silicon design stages.
With the growing complexity and gradually shrinking power requirements In system-on-chip designs, sophisticated architectural power management policies are commonplace. Comprehensive validation of the power management strategy in an integrated circuit involving both the digital power manager with analog power control circuitry is crucial. Formal verification reveals critical bugs due to such erroneous power management activities leading to the disrupted operability of a design.
Safety-critical embedded control systems are designed with specific reliability targets, and design practices include the appropriate allocation of both spatial and temporal redundancies In implementation to meet such requirements. These redundancy artefacts are realized leveraging the formal properties of the error-free system, the error probabilities of the control components, and the reliability target. Upfront formal analysis of redundancy specifications aids in budgeting the resource requirements from a cost versus reliability perspective and also identifies the reliability gaps.
Formal methods are widely adopted in understanding the vulnerabilities (with respect to fault attacks) of cryptographic premitives in secure cipher designs. Consequently, automatic countermeasures can be provided to protect the mal-access from the attacker exploiting these vulnerable spots. Automated CAD frameworks and tools are built to comprehensively assess and mitigate security flaws in cipher algorithms as well as their hardware or software implementations.
Developing strong PUF designs resilient to machine learning attacks is an important necessity for wider adoption of PUFs. Theoretical proofs are formally chalked out to justify the responsiveness, unclonability, reliability, correlation and learnability factors of a PUF design. CAD based testability and formal learnability analysis frameworks are necessary for comprehensively assessing the strength of any PUF design or its compositional derivatives.
Explainability is becoming one of the key needs for widespread adoption of ML approaches in safety-critical applications. It is becoming imperative to explore and devise approaches for comprehensive interpretability as well as ensure robustness so that it cannot be fooled by adversarial perturbations.



[ Please Visit Formal Methods Research Group Page for More Details ]

Publications

"If you have done something good, try to write. If you have written something proper, try to publish. If you have published well, try to write a thesis."    – Anonymous

Some Recent Publications:


MADelO : A Modelling and Assessment Framework for Delay PUFs leveraging Gradient-based Optimization Techniques.
Durba Chatterjee, Debdeep Mukhopadhyay and Aritra Hazra.
Accepted in IEEE Computer Society Annual Symposium on VLSI (ISVLSI), pp. X-Y, July 2025.

PARLE-G : Provable Automated Representation and Analysis Framework for Learnability Evaluation of Generic PUF Compositions.
Durba Chatterjee, Aritra Hazra and Debdeep Mukhopadhyay.
In IEEE Transactions on Computers (TC), vol. 74, No. 3, pp. 820-834, March 2025.

Formal Methods for Characterization and Analysis of Quality Specifications in Component-based Systems.
Aritra Hazra.
In International Journal of Reliability, Quality and Safety Engineering (IJRQSE), vol. 32, No. 1, pp. 2450044, February 2025.

SISCO: Selective Invariant Sharing, Clustering and Ordering for Effective Multi-Property Formal Verification.
Sourav Das, Aritra Hazra, Pallab Dasgupta, Himanshu Jain and Sudipta Kundu.
In 30th Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 1343-1349, January 2025.

PrOFraC: Property Ordering and Frame Clause Reuse for Multi-Property Verification.
Sourav Das, Aritra Hazra, Pallab Dasgupta, Himanshu Jain and Sudipta Kundu.
In 38th International Conference on VLSI Design (VLSID), pp. 7-12, January 2025.
Nominated for the BEST STUDENT PAPER.

ReFrame: Rectification Framework for Image Explaining Architectures.
Debjyoti Das Adhikary, Aritra Hazra and Partha Pratim Chakrabarti.
In 8th International Conference on Data Science and Management of Data (CODS-COMAD), pp. X-Y, December 2024.

PURSE: Property Ordering Using Runtime Statistics for Efficient Multi-Property Verification.
Sourav Das, Aritra Hazra, Pallab Dasgupta, Sudipta Kundu and Himanshu Jain.
In 27th Design, Automation and Test in Europe Conference (DATE), pp. 1-6, March 2024.

Systematically Quantifying Cryptanalytic Nonlinearities in Strong PUFs.
Durba Chatterjee, Kuheli Pratihar, Aritra Hazra, Ulrich Rührmair and Debdeep Mukhopadhyay.
In IEEE Transactions on Information Forensics and Security (TIFS), vol. 19, pp. 1126-1141, November 2023.

Explainable Decision Tree-based Screening of Cognitive Impairment Leveraging Minimal Neuropsychological Tests.
Km Poonam, Ayush Prasad, Rajlakshmi Guha, Aritra Hazra and Partha Pratim Chakrabarti.
In 10th International Conference on Pattern Recognition and Machine Intelligence (PReMI), pp. 241-251, December 2023.

Analog Coverage-driven Selection of Simulation Corners for AMS Integrated Circuits.
Sayandeep Sanyal, Aritra Hazra, Pallab Dasgupta, Scott Morrison, Sudhakar Surendran, Lakshmanan Balasubramanian and Mohammad Rahman.
In 26th Design, Automation and Test in Europe Conference (DATE), pp. 1-6, April 2023.

CoVerPlan: A Comprehensive Verification Planning Framework leveraging PSS Specifications.
Sourav Das, Sayandeep Sanyal, Aritra Hazra and Pallab Dasgupta.
In ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 28, no. 1, pp. 9:1-32, January 2023.

Towards Adversarial Purification using Denoising AutoEncoders.
Dvij Kalaria, Aritra Hazra and Partha Pratim Chakrabarti.
In the NeurIPS ML Safety Workshop, December 2022.

The CoveRT Approach for Coverage Management in Analog and Mixed Signal Integrated Circuits.
Sayandeep Sanyal, Pallab Dasgupta, Aritra Hazra, Sourav Das, Scott Morrison, Sudhakar Surendran and Lakshmanan Balasubramanian.
In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), vol. 41, no. 12, pp. 5695-5708, December 2022.

Physically Related Functions: Exploiting Related Inputs of PUFs for Authenticated-Key Exchange.
Durba Chatterjee, Harishma Boyapally, Sikhar Patranabis, Urbi Chatterjee, Aritra Hazra and Debdeep Mukhopadhyay.
In IEEE Transactions on Information Forensics and Security (TIFS), vol. 17, pp. 3847-3862, October 2022.

  • Synthesis of Sampling Modes for Adaptive Control.   [ C9 ]
    Rajorshee Raha, Aritra Hazra, Akash Mondal, Soumyajit Dey, Partha Pratim Chakrabarti and Pallab Dasgupta.
    In 4th IEEE International Conference on Control System, Computing and Engineering (ICCSCE), pp. 294-299, November 2014.

                                                                               

Patents

"Patents are like fertilizer. Applied wisely and sparingly, they can increase growth."    – Alex Tabarrok

United States Patent No. US2024/0193337A1

  • Title:   Tracking Coverage Artifacts for Periodic Signals using Sequence-based Abstractions
  • Inventors:   Ayan Chakraborty, Sayandeep Sanyal, Pallab Dasgupta, Aritra Hazra, Scott Morrison, Sudhakar Surendran, Lakshmanan Balasubramanian and Mohammad Moshiur Rahman
  • Status:   Granted
  • Application No.:   US18/076,547
  • Filing Date:   07-December-2022
  • Issuing Date:   13-June-2024

    • United States Patent No. US2023/0176100A1

  • Title:   Identifying Glitches and Levels in Mixed-Signal Waveforms
  • Inventors:   Sayandeep Sanyal, Pallab Dasgupta, Aritra Hazra, Scott Morrison, Sudhakar Surendran and Lakshmanan Balasubramanian
  • Status:   Granted
  • Application No.:   US18/071,917
  • Filing Date:   30-November-2022
  • Issuing Date:   08-June-2023

    • Invited Talks

    "If you can't explain it simply, you don't understand it well enough."    – Albert Einstein

    2025 February:  Formal Methods for Comprehensive Validation of On-Chip Architectural Power Management   (HPC-RISC Fusion Workshop, BITS-Pilani, Hyderabad)
    2024 July:   AI in Strategic Game Playing   (Workshop on HPC and AIm, Centre for Computational and Data Sciences, IIT Kharagpur)
    2024 March:   Learning to Become Experts in Playing Games: A Time-Traversal through AI Eras   (Keynote in ACM Eminent Speaker Program, RAIT ACM Student Chapter, Navi Mumbai)
    2023 July:   Policy Optimization in Reinforcement Learning   (Short-Term Online Course on Digital Supply Chain Management, National Institute of Technology, Calicut)
    2023 June:   Tryst with Infinity: A Mathematical Poetry   (Summer Science Workshop by Science Centre (Midnapore), Raja Narendralal Khan Women’s College, Midnapore)
    2019 December:   Formal Verification for CPS Security Assurance   (Targeted Workshop on Cyber Physical System Security (CPSS), IIT Kharagpur)
    2018 July:   PAC Learnability of PUFs   (Workshop on Security In Connected World (WSPSCW), IIT Kharagpur)
    2018 July:   Formal Methods for Fault Attack Vulnerability Analysis in Block Ciphers   (Workshop on Security In Connected World (WSPSCW), IIT Kharagpur)
    2017 March:   Formal Methods for Security Analysis   (UTokyo - IIT Madras Workshop on Theoretical Computer Science, IIT Madras)
    2016 June:   Formal Methods for Power Intent Verification   (ISI Kolkata)
    2014 March:   Design of Reliable Embedded Control Systems   (Workshop on High Assurance Embedded Control Software, IIT Kharagpur)

    Note to Aspiring Applicants

    "Study hard what interests you the most In most undisciplined, irreverent and original manner possible."    – Richard Feynman

    • Post-Doctoral Positions:   The Institute has a regularized procedure to appoint post-doctoral researchers. For details, please visit HERE. To apply, please visit HERE. (Interested candidates may write to me with a copy of their recent resume and one letter of recommendation.)

    • Ph.D. Positions:   The Institute has a centralized policy for PhD entrance. For details, please visit HERE. To apply, please visit HERE. The syllabus for the PhD entrance test (in CSE-Dept) can be found HERE.

    • M.S. (by Research) Positions:   For M.S., you have to first get through some project. The institute project advertisements appear HERE. Once you are already a project staff, you can apply for MS. The syllabus for the MS entrance test (in CSE-Dept) can be found HERE.

    • Internship Positions:   We only offer summer internships and hence please do not apply for internships in winter/fall. For details, please visit HERE. To apply, please visit HERE. (In general, your internship requests directly to my mail-box will never be acknowledged! Therefore, kindly apply ONLINE.)

    Contact

    Designation:   Assistant Professor

    Office:   CSE-102   (Ground-Floor)

    Email:   aritrah [at] cse [dot] iitkgp [dot] ac [dot] in

    Phone:   +91-3222-304640   (Extn: 84640)




    Address:

        Department of Computer Science and Engineering,

        Indian Institute of Technology Kharagpur,

        Paschim Medinipur, West Bengal 721302, INDIA.


    http://www.iitkgp.ac.in/department/CS/faculty/cs-aritrah

    © Aritra Hazra   |   Last Updated: June 2025