About Me

Hello! I am Soumyadip Bandyopadhyay, currently working as a Scientist at the ABB Corporate Research Lab since July 2023. My current research focuses on the verification of PLC programs during software migration and upgrades, validation of Generative AI outputs, and pioneering methods in forward engineering using Large Language Models (LLMs). At ABB, I am proud to be part of a global innovation ecosystem that blends engineering excellence with cutting-edge research.

I earned my Ph.D. from the prestigious Indian Institute of Technology, Kharagpur (IIT Kharagpur), specializing in Formal Methods and Software Engineering. My doctoral studies cultivated a deep interest in rigorous system design, verification, and advanced software development techniques.

Following my Ph.D., my professional journey began as a Postdoctoral Researcher at the renowned Hasso Plattner Institute in Germany. There, I had the opportunity to deepen my research expertise, collaborate internationally, and contribute to innovative research projects in software verification and model checking.

Subsequently, I embraced academia, serving as an Assistant Professor at BITS Pilani, Goa Campus for 3.5 enriching years. During this time, I mentored students, published several research papers in reputed international conferences and journals, and contributed to the scientific community by serving as a Program Committee Member and Reviewer for various esteemed conferences and journals.

With a spirit of exploration, I transitioned to industry and joined NVIDIA as a Senior Formal Verification Engineer. At NVIDIA, I worked on Data Path Verification (DPV) using state-of-the-art tools such as VC Formal and JasperGold, contributing to the development of reliable and high-performance hardware verification solutions.

Outside of my professional life, I am passionately interested in world politics and the rich traditions of folk music. I also find joy in writing poetry and performing heartfelt recitations, allowing me to creatively express my thoughts and emotions.

Contact Information

Scientist

Mobile: +91 8900270263

ABB Corporate Research
Official Email: soumyadip.bandyopadhyay@in.abb.com

Country: India
Personal Email: soumyadipcse@gmail.com

  • My Resume
  • Education a

    Indian Institute of Technology, Kharagpur, West Bengal, India (2009–2017)

    • Ph.D. in Computer Science and Engineering
    • Formal Verification Research Group
    • Thesis: Path Based Equivalence Checking of Petri Net Representation of Programs for Translation Validation - View Thesis

    West Bengal University of Technology, Kolkata, West Bengal, India (2004–2008)

    • B.Tech in Computer Science and Engineering

    Work Experience

    • Research Scientist, ABB Corporate Research (July 2023 – Present)
    • Senior Formal Verification Engineer, NVIDIA (May 2022 – June 2023)
    • Assistant Professor, BITS Pilani K K Birla Goa Campus (Dec 2018 – May 2022)
    • Post-Doctoral Fellow, System Analysis and Modeling Group, Hasso Plattner Institute, Germany (Aug 2017 – Oct 2018)
    • Assistant Professor, BITS Pilani K K Birla Goa Campus (Dec 2016 – July 2017)
    • Visiting faculty, BITS Pilani K K Birla Goa Campus (Sep 2015 – Dec 2016)

    Research Interests

    • Formal Methods
    • Program Equivalence
    • Software Verification
    • Generative AI
    • PLC Verification
    • Data Path Verification
    • High-Level Synthesis
    • Model-Driven Engineering

    Sponsored and Consultancy Projects

    • "APP based learning for Python program"
      Funding Agency: 6th Sense and AGH advisor
      Duration: 2021-2023
      Amount: 15.81L
    • "Modelling and Verification of Bio-Inspired system"
      Funding Agency: DST under BIO-CPS incubation
      Duration: 2020-2025
      Amount: 40L
    • "AES: Automated Evaluation Systems for Computer Programming Course in Any University"
      Funding Agency: BITS Pilani
      Duration: 2018-2021
      Project Amount: 2L
    • “SamaTulyata: Automated Evaluation for Computer Programming Course”
      Funding Agency: TLC BITS Goa
      Duration: 2019-2020
      Project Amount: 1L

    Industrial Projects

    • CodeGenAI: Explore potential of Generative AI and Large Language Model (LLM) to support engineering:(ETFA 2024)
      • Generation of control logic utilizing ABB control libraries and ABB notations.
      • Generation of test code to improve quality and save efforts in FAT.
      • Streamlined and integrated user interface to let control engineer interact with GenAI.
    • GenAi4SamaTulyata: Proving the the functional equivalecne for Software Migration and Software evolve:(FSE 2025 Poster Track)
      • Building a tool for equivalence checker for software migration and software evolve.
      • Model constructor carried out by LLM and verified for correctness using formal verification tools.
      • Check LLM hallucination using automated reaseon method.

    Journal Publications

    1. Soumyadip Badyopadhyay, Dipankar Sarkar, Chittaranjan Mandal, Holger Giese, "Translation Validation of Coloured Petri Net Models of Programs on Integers", Acta Informatica, Vol. 59, Issue: 3, Pages: 725-759
    2. Soumyadip Badyopadhyay, Dipankar Sarkar, Chittaranjan Mandal, "Equivalence checking of Petri net models of programs using static and dynamic cut-points", Acta Informatica, Vol. 54, Issue: 4, Pages: 321-381
    3. Soumyadip Bandyopadhyay, Dipankar Sarkar, Kunal Banerjee, Chittaranjan A. Mandal, Krishnam Raju, "A Path Construction Algorithm for Translation Validation using PRES+ Models", Parallel Processing Letters, Vol. 26, Issue: 2, Pages: 1-18

    Conference and Workshop Publications

    1. Soumyadip Bandyopadhyay and Raoul Jetley, "Pn4PLC: Verification of Software Upgrade for PLC Code", FSE 2025 (Core rank A*)
    2. Md Tauseef Alam, Sorbajit Goswami, Khushi Singh, Raju Halder, Abyayananda Maiti, Soumyadip Bandyopadhyay, "SolGen: Secure Smart Contract Code Generation Using Large Language Models Via Masked Prompting", ISEC 2025
    3. Heiko Koziolek, Virendra Ashiwal, Soumyadip Bandyopadhyay, Chandrika K R, "Automated Control Logic Test Case Generation using Large Language Models", ETFA 2024
    4. Rakshit Mittal, Dominique Blouin, Anish Bhobe, and Soumyadip Bandyopadhyay, "Solving the Instance Model-View Update Problem in AADL", MODELS 2022 (Core rank A)
    5. Rakshit Mittal, Dominique Blouin, Soumyadip Bandyopadhyay, "PNPEq: Verification of Scheduled Conditional Behavior in Embedded Software", APSEC 2021 (during publication Core rank B)
    6. Rakshit Mittal, Rochishnu Banerjee, Dominique Blouin, Soumyadip Bandyopadhyay, "Towards an Approach for Translation Validation of Thread-level Parallelizing Transformations using Colored Petri Nets", ICSOFT 2021 (Best Paper) (during publication Core rank B)
    7. Rakshit Mittal, Rochisnu Banerjee, Santonu Sarkar, Soumyadip Bandyopadhyay, "Translation Validation of Loop involving Code Optimizing Transformations using Petri Net based Models of Programs", Petri Nets workshop 2020
    8. Shivam, Nilanjana Goswami, Veeky Baths, Soumyadip Bandyopadhyay, "AES: Automated Evaluation Systems for Computer Programming Course", ICSOFT 2019 (during publication Core rank B)
    9. Soumyadip Bandyopadhyay, Dipankar Sarkar, Chittaranjan Mandal, "SamaTulyataOne: A Path Based Equivalence Checker", ISEC 2019
    10. Santonu Sarkar, Prateek Kandelwal, Soumyadip Bandyopadhyay, Holger Giese, "Analysis of GPGPU Programs for Data-race and Barrier Divergence", ICSOFT 2018 (during publication Core rank B)
    11. Soumyadip Bandyopadhyay, Santonu Sarkar, Dipankar Sarkar, and Chittaranjan Mandal, "SamaTulyata, An Efficient Path Based Equivalence Checking Tool", ATVA 2017 (during publication Core rank A)
    12. Soumyadip Bandyopadhyay, Santonu Sarkar, and Kunal Banerjee, "An End-to-End Formal Verifier for Parallel Programs", ICSOFT 2017 (during publication Core rank B)
    13. Soumyadip Bandyopadhyay and Kunal Banerjee, "PRESGen: A Fully Automatic Equivalence Checker for Validating Optimizing and Parallelizing Transformations", HPDC workshop 17
    14. Soumyadip Bandyopadhyay, Dipankar Sarkar, and Chittaranjan Mandal, "An efficient path based equivalence checking for Petri net based models of programs", ISEC-2016
    15. Soumyadip Bandyopadhyay and Kunal Banerjee, "Implementing an Efficient Path Based Equivalence Checker for Parallel Programs", HPDC workshop 16
    16. Kunal Banerjee, Soumyadip Bandyopadhyay, and Santonu Sarkar, "Data-Race Detection: The Missing Piece for an End-to-End Semantic Equivalence Checker for Parallelizing Transformations of Array-Intensive Programs", PLDI workshop 2016
    17. Soumyadip Bandyopadhyay, Dipankar Sarkar, and Chittaranjan Mandal, "Validating SPARK: High Level Synthesis compiler", ISVLSI-2015
    18. Soumyadip Bandyopadhyay, Dipankar Sarkar, and Chittaranjan Mandal, "A Path-Based Equivalence Checking Method for Petri net based Models of Programs", ICSOFT-EA-2015 (during publication Core rank B)
    19. Soumyadip Bandyopadhyay, Dipankar Sarkar, Chittaranjan A. Mandal, "An Efficient Equivalence Checking Method for Petri net based Models of Programs", ICSE 2015 (Core rank A*)
    20. Soumyadip Bandyopadhyay, Kunal Banerjee, Dipankar Sarkar, Chittaranjan A. Mandal, "Translation Validation for PRES+ Models of Parallel Behaviours via an FSMD Equivalence Checker", VDAT 2012

    Poster Publications

    1. Soumyadip Bandyopadhyay, "Behavioural verification using Petri net based models of programs", POPL-2015 (ACM student research competition)
    2. Soumyadip Bandyopadhyay, Dipankar Sarkar, Chittaranjan A. Mandal, "Translation Validation using Path-Based Equivalence Checking of Petri net based Models of Programs", WEPL 2015

    Book Chapters

    1. Bedir Tekinerdogan, Rakshit Mittal, Rima Al-Ali, Mauro Iaconod, Eva Navarroe, Soumyadip Bandyopadhyay, Ken Vanherpen, and Ankica Barisic, "A feature-based ontology for cyber physical systems", Chapter 3, Book Title: Multi-Paradigm Modelling Approaches for Cyber-Physical, Elsevier Press. ISBN No. 9780128191064
    2. Holger Giese, Dominique Blouin, Rima Al-Ali, Hana Mkaoua, Soumyadip Bandyopadhyay, Mauro Iacono, Moussa Amrani, Stefan Klikovits, and Ferhat Erata, "An ontology for multiparadigm modelling", Chapter 4, Book Title: Multi-Paradigm Modelling Approaches for Cyber-Physical, Elsevier Press. ISBN No. 9780128191064
    3. Dominique Blouin, Rima Al-Ali, Holger Giese, Stefan Klikovits, Soumyadip Bandyopadhyay, Ankica Barisic, and Ferhat Erata, "An integrated ontology for multi-paradigm modelling for cyber-physical systems", Chapter 5, Book Title: Multi-Paradigm Modelling Approaches for Cyber-Physical, Elsevier Press. ISBN No. 9780128191064

    Talk

    1. "SamaTulyata4PLC: Behavioural Verification of Software Upgrade and Migration for PLC Code using Petri net based Model", FM Update 2024
    2. "Industrial Application of Equivalence checking of programs", RHPL 2024 (co-located with FSTTCS 2023)
    3. "Equivalence checking of Programs for Translation Validation", FM Update 2023
    4. "Implementing a Path Based Equivalence Checker for Petri net based Models of Programs", PERR 2022
    5. "Equivalence checking of Petri net based models of programs", Telecom Paris, France 2022
    6. "Translation Validation of Loop involving Code Optimizing Transformations using Petri Net based Models of Programs", FM Update 2021
    7. "Translation Validation using CPN Models of Programs", CMI 2017

    Tools

    • SamaTulyata - Petri net Based Formal equivalence checker for C Programs
    • SamaTulyata4PLC - Software Migration Verifier for PLC programs
    • AutoVal - Automated Evaluation fortware for Computer Programing course

    Video

    Honours and Awards

    • Finalist Processo Automation Hackathon 2024
    • Best Paper, ICSOFT 2021
    • Selected in 7th HLF as top 50 young researcher in computer science
    • Post-Doctoral Fellowship, Hasso Plattner Institute, Germany, 2017
    • TCS Innovation Lab Research Fellowship, 2012
    • Czech Republic Scholarship, 2007

    Professional Activities

    • Reviewer at:
      • CAV-2014
      • EMSOFT-2015
      • DAC 2020
      • ACM TOSEAM
      • Acta Informatica
    • PC member:
      • ISEC 2018-2025
      • ICSOFT 2018–2023
      • VLSI D 2023
      • MPM4CPS 2021–2023
      • ModeVa 2023-2024
      • VDAT 2025
    • Senior IEEE Member, ACM Member
    • Organiser
      • PERR 2022 (co-located with CAV 2022)
      • PEQ 2022 (co-located with ISEC 2022)
      • SE4AI 2021 (co-located with ISEC 2021)
      • SE4AI 2020 (co-located with ISEC 2021)
      • CTiCPS 2020