Dr. Soumyadip Bandyopadhyay
Assistant Professor · Ashoka University · IIT Kharagpur Ph.D. · Formal Methods & AI
🔬 Formal Verification
🤖 Neurosymbolic AI
⚙️ Industrial Automation
📐 Software Engineering
Biography
Hello! I am Soumyadip Bandyopadhyay, currently working as an Assistant Professor in the Department of Computer Science at Ashoka University. My research interests span Formal Methods, Software Engineering, Industrial Automation, and Neurosymbolic AI. My current work focuses on formal verification, AI-assisted software engineering, and building trustworthy AI systems.
I earned my Ph.D. from IIT Kharagpur, specializing in Formal Methods and Software Engineering. My professional journey began with a Postdoctoral Research Fellowship at the Hasso Plattner Institute, Germany, followed by serving as an Assistant Professor at BITS Pilani, K. K. Birla Goa Campus. I then joined NVIDIA as a Senior Formal Verification Engineer, where I worked on Data Path Verification using VC Formal and JasperGold. Subsequently, I worked as a Research Scientist at the ABB Corporate Research Center, India, conducting research on PLC program verification, validation of Generative AI outputs, and LLM-driven software engineering.
Outside my professional life, I enjoy following world politics, listening to folk music, writing poetry, and performing recitations.
Contact Information
Position
Assistant Professor
Mobile
+91 8900270263
Official Email
Personal Email
Location
India 🇮🇳
Organization
Ashoka University
Education & Work Experience
Education
Ph.D. · Jan 2009 – Aug 2017
Indian Institute of Technology, Kharagpur
West Bengal, India · CSE · Formal Verification Research Group
Thesis: Path Based Equivalence Checking of Petri Net Representation of Programs for Translation Validation View Thesis
B.Tech · Jul 2004 – Aug 2008
West Bengal University of Technology, Kolkata
West Bengal, India · Computer Science and Engineering
Work Experience
Ashoka University
Assistant Professor
August 2026 – PresentABB Corporate Research
Research Scientist
July 2023 – July 2026NVIDIA
Senior Formal Verification Engineer
May 2022 – June 2023BITS Pilani K K Birla Goa Campus
Assistant Professor
Dec 2018 – May 2022Hasso Plattner Institute, Germany
Post-Doctoral Fellow · System Analysis and Modeling Group
Aug 2017 – Oct 2018BITS Pilani K K Birla Goa Campus
Assistant Professor
Dec 2016 – July 2017BITS Pilani K K Birla Goa Campus
Visiting Faculty
Sep 2015 – Dec 2016Advance VLSI Lab IIT Kharagpur
Junior Project Assistant
Aug 2008 – Jul 2012Research Interests & Projects
Research Interests
Industrial Projects
CodeGenAI
- Generation of control logic using ABB control libraries and notations.
- Generation of test code to improve quality and save FAT efforts.
- Streamlined UI for control engineers to interact with GenAI.
GenAI4SamaTulyata
- Tool for equivalence checker for software migration and evolution.
- Model constructor by LLM, verified using formal verification tools.
- LLM hallucination detection via automated reasoning methods.
Sponsored & Consultancy Projects
"APP based learning for Python program"
"Modelling and Verification of Bio-Inspired System"
"AES: Automated Evaluation Systems for Programming Course"
"SamaTulyata: Automated Evaluation for Programming Course"
Publications
Journal Publications 3
1Soumyadip Bandyopadhyay, D. Sarkar, C. Mandal, H. Giese, "Translation Validation of Coloured Petri Net Models of Programs on Integers", Acta Informatica, Vol.59, Issue:3, pp.725–759.
2Soumyadip Bandyopadhyay, D. Sarkar, C. Mandal, "Equivalence checking of Petri net models using static and dynamic cut-points", Acta Informatica, Vol.54, Issue:4, pp.321–381.
3Soumyadip Bandyopadhyay, D. Sarkar, K. Banerjee, C.A. Mandal, K. Raju, "A Path Construction Algorithm for Translation Validation using PRES+ Models", Parallel Processing Letters, Vol.26, Issue:2, pp.1–18.
Conference & Workshop Publications 24
1A. Mukherjee Soumyadip Bandyopadhyay R. Halder and D. Blouin, "Don’t Just Translate: Verify - LLM-Guided Solidity Migration with Semantic Guarantees", ICSOFT 2026
2Soumyadip Bandyopadhyay and S. Sarkar, "Antarbhukti: Verifying Correctness of PLC Software during System Evolution", ATVA 2025 Core B
3Soumyadip Bandyopadhyay and R. Jetley, "Pn4PLC: Verification of Software Upgrade for PLC Code", FSE 2025 Core A★
4Md T. Alam et al. and Soumyadip Bandyopadhyay, "SolGen: Secure Smart Contract Code Generation Using LLMs Via Masked Prompting", ISEC 2025
5H. Koziolek, V. Ashiwal, Soumyadip Bandyopadhyay and C.K.R, "Automated Control Logic Test Case Generation using LLMs", ETFA 2024
6R. Mittal, D. Blouin, A. Bhobe and Soumyadip Bandyopadhyay, "Solving the Instance Model-View Update Problem in AADL", MODELS 2022 Core A
7R. Mittal, D. Blouin, Soumyadip Bandyopadhyay, "PNPEq: Verification of Scheduled Conditional Behavior in Embedded Software", APSEC 2021 Core B
8R. Mittal, D. Blouin, Soumyadip Bandyopadhyay, "Validating Extended Feature Model Configurations using Petri Nets", Petri Nets Workshop 2021
9R. Mittal and Soumyadip Bandyopadhyay, "Translation Validation of Scheduled Conditional Behavior using PN", Petri Nets Workshop 2021
10R. Mittal, R. Banerjee, D. Blouin, Soumyadip Bandyopadhyay, "Translation Validation of Thread-level Parallelizing Transformations using CPNs", ICSOFT 2021 🏆 Best Paper Core B
11R. Mittal et al. and Soumyadip Bandyopadhyay, "Translation Validation of Loop Optimizing Transformations using PN", Petri Nets Workshop 2020
12Shivam, N. Goswami, V. Baths, Soumyadip Bandyopadhyay, "AES: Automated Evaluation Systems for Programming Course", ICSOFT 2019 Core B
13Soumyadip Bandyopadhyay, D. Sarkar, C. Mandal, "SamaTulyataOne: A Path Based Equivalence Checker", ISEC 2019
14S. Sarkar, P. Kandelwal, Soumyadip Bandyopadhyay, H. Giese, "Analysis of GPGPU Programs for Data-race and Barrier Divergence", ICSOFT 2018 Core B
15Soumyadip Bandyopadhyay, S. Sarkar, D. Sarkar, C. Mandal, "SamaTulyata, An Efficient Path Based Equivalence Checking Tool", ATVA 2017 Core A
16Soumyadip Bandyopadhyay, S. Sarkar, K. Banerjee, "An End-to-End Formal Verifier for Parallel Programs", ICSOFT 2017 Core B
17Soumyadip Bandyopadhyay and K. Banerjee, "PRESGen: A Fully Automatic Equivalence Checker for Optimizing and Parallelizing Transformations", HPDC Workshop 2017
18Soumyadip Bandyopadhyay, D. Sarkar, C. Mandal, "An efficient path based equivalence checking for PN models", ISEC 2016
19Soumyadip Bandyopadhyay and K. Banerjee, "Implementing an Efficient Path Based Equivalence Checker for Parallel Programs", HPDC Workshop 2016
20K. Banerjee, Soumyadip Bandyopadhyay, S. Sarkar, "Data-Race Detection for End-to-End Semantic Equivalence Checker", PLDI Workshop 2016
21Soumyadip Bandyopadhyay, D. Sarkar, C. Mandal, "Validating SPARK: High Level Synthesis compiler", ISVLSI 2015
22Soumyadip Bandyopadhyay, D. Sarkar, C. Mandal, "A Path-Based Equivalence Checking Method for PN Models", ICSOFT-EA 2015 Core B
23Soumyadip Bandyopadhyay, D. Sarkar, C.A. Mandal, "An Efficient Equivalence Checking Method for PN Models", ICSE 2015 Core A★
24Soumyadip Bandyopadhyay, K. Banerjee, D. Sarkar, C.A. Mandal, "Translation Validation for PRES+ Models via FSMD Equivalence Checker", VDAT 2012
Poster Publications 2
1Soumyadip Bandyopadhyay, "Behavioural verification using PN models of programs", POPL 2015 – ACM Student Research Competition
2Soumyadip Bandyopadhyay, D. Sarkar, C.A. Mandal, "Translation Validation using Path-Based Equivalence Checking of PN Models", WEPL 2015
Book Chapters 3
1B. Tekinerdogan, R. Mittal, R. Al-Ali, ..., Soumyadip Bandyopadhyay, et al., "A feature-based ontology for cyber physical systems", Chapter 3, Multi-Paradigm Modelling Approaches for Cyber-Physical, Elsevier. ISBN: 9780128191064
2H. Giese, D. Blouin, R. Al-Ali, ..., Soumyadip Bandyopadhyay, et al., "An ontology for multiparadigm modelling", Chapter 4, Multi-Paradigm Modelling Approaches for Cyber-Physical, Elsevier. ISBN: 9780128191064
3D. Blouin, R. Al-Ali, H. Giese, ..., Soumyadip Bandyopadhyay, et al., "An integrated ontology for multi-paradigm modelling for CPS", Chapter 5, Multi-Paradigm Modelling Approaches for Cyber-Physical, Elsevier. ISBN: 9780128191064
Tools & Talks
Invited Talks
1
"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" — 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 PN Models" — FM Update 2021
7
"Translation Validation using CPN Models of Programs" — CMI 2017
Open Source Tools
Achievements & Professional Activities
Honours & Awards
Finalist — Process Automation Hackathon 2024
Best Paper Award — ICSOFT 2021
Selected in 7th Heidelberg Laureate Forum (HLF) — Top 50 Young Researcher in CS
Post-Doctoral Fellowship — Hasso Plattner Institute, Germany, 2017
TCS Innovation Lab Research Fellowship, 2012
Czech Republic Scholarship, 2007
Reviewer
- CAV 2014
- EMSOFT 2015
- DAC 2020
- ACM TOSEAM
- IEEE Software
- Acta Informatica
Program Committee
- ISEC 2018–2025
- ICSOFT 2018–2023
- VLSI D 2023-2025
- MPM4CPS 2021–2023 (co-located MODELS)
- ModeVa 2023–2026 (co-located MODELS)
- PERR 2026 (co-located CAV 2026)
Organizer
- PERR 2022 (co-located CAV 2022)
- PEQ 2022 (co-located ISEC 2022)
- SE4AI 2021 (co-located ISEC 2021)
- SE4AI 2020 (co-located ISEC 2020)
- CTiCPS 2020 ↗
Memberships
- IEEE Member
- ACM Member