About Me

I am a research scientist advancing AI reasoning, and general intelligence, with a strong emphasis on interpretability, safety, and alignment. My work focuses on neuro-symbolic AI, integrating formal methods, mathematical logic, and program synthesis to design AI systems that are not only interpretable but also capable of robust reasoning, cross-domain generalization, and solving open-ended problems.

Research Interests

LLM Reasoning, AI for Code, Neuro-symbolic AI, Formal Methods

Research Projects

• Automating formal methods from natural-language specifications using agentic AI.
• Detecting unhandled error conditions in real-world codebases using agentic AI.
• Generating interpretable models, like Decision Trees, using Large Language Models.
• Extracting state machines from programs using Large Language Models.
• LLM assisted heterogeneous computing programming.

Employment

• Software Engineering Institute | Carnegie Mellon University

  
  

  Research Scientist

  : May 2023 to October 2025.

• Tufts University

  
  

  Postdoctoral Researcher, under Prof. Jeff Foster

  : August 2020 to September 2021.
  Synthesizing programs from modular program blocks, using row-type inferencing, symbolic solving, and genetic programming.

• Runtime Verification

  
  

  Research Internship

  : June 2020 to August 2020.
  Verification of Solidity bytecode for smart contracts used in the Ethereum Blockchain.

Education

• Integrated Ph.D., Computer Science

  
  University of Illinois at Urbana-Champaign, December 2019
  Research Projects:
  • Specification Mining: Generating precise contracts for C# programs.
  • Precondition Synthesis: Synthesized preconditions to prevent failures in C# programs.
  • Invariant Synthesis: Verified GPU and heap programs by synthesizing loop invariants.
  • Program Synthesis: Developed a synthesis engine that solved SyGuS benchmarks.
  • Network Synthesis: Automated SDN configuration changes to enforce policy updates.
  • Problem Synthesis: Designed a language for generating parameterized problem variants.

• Master of Science, Computer Science

  
  Chennai Mathematical Institute, August 2011

Publications

• Towards Compositional Assurance of Large Cyber-Physical Systems

    PDF
  Gabriel A. Moreno, Mark Klein, Shambwaditya Saha, Farzaneh Derakhshan, Limin Jia
  Proceedings of the 1st Workshop on Formal Arguments for Cps Certification (FACCT), 2025.

• Synthesizing Contracts Correct Modulo a Test Generator *

    PDF
  Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felica Wang, P. Madhusudan, Tao Xie
  ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2021.

• A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines

    PDF
  Daniel Neider, P. Madhusudan, Shambwaditya Saha, Pranav Garg, Daejun Park
  Journal of Automated Reasoning (JAR), 2020. Invited Article

• Learning Stateful Preconditions Modulo a Test Generator *

    PDF
  Angello Astorga, P. Madhusudan, Shambwaditya Saha, Shiyu Wang, Tao Xie
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2019.

• Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants

    PDF
  Daniel Neider, Shambwaditya Saha, Pranav Garg, P. Madhusudan
  International Static Analysis Symposium (SAS), 2019.

• Compositional Synthesis of Piece-Wise Functions by Learning Classifiers *

    PDF
  Daniel Neider, Shambwaditya Saha, P. Madhusudan
  ACM Transactions on Computational Logic (TOCL), 2018. Invited Article

• A Decidable Fragment of Second Order Logic With Applications to Synthesis *

    PDF
  P. Madhusudan, Umang Mathur, Shambwaditya Saha, Mahesh Viswanathan
  EACSL Conference Computer Science Logic (CSL), 2018.

• Invariant Synthesis for Incomplete Verification Engines

    PDF
  Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha, Daejun Park
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2018.

• Synthesizing Piece-Wise Functions by Learning Classifiers *

    PDF
  Daniel Neider, Shambwaditya Saha, P. Madhusudan
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016.

• Alchemist: Learning Guarded Affine Functions *

    PDF
  Shambwaditya Saha, Pranav Garg, P. Madhusudan
  International Conference on Computer Aided Verification (CAV), 2015.

• NetGen: Synthesizing Data-plane Configurations for Network Policies *

    PDF
  Shambwaditya Saha, Santhosh Prabhu, P. Madhusudan
  ACM SIGCOMM Symposium on Software Defined Networking Research (SOSR), 2015.

• Syntax-Guided Synthesis *

    PDF
  Rajeev Alur, Rastislav Bodik, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas KressGazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa
  Dependable Software Systems Engineering, NATO Science for Peace, Security Series., 2015. Invited Article

Thesis

• Learning Frameworks for Program Synthesis

    PDF
  Ph.D. Dissertation, University of Illinois at Urbana-Champaign, 2019
  Advisor: Prof. Madhusudan Parthasarathy

• A Survey of Automata and Logics Over Infinite Graphs

    PDF
  Master's Thesis, Chennai Mathematical Institute, 2011
  Advisor: Prof. K. Narayan Kumar

Tools

• Precis

  : Synthesizes postconditions of C# programs using the test generator PEX.

• Provisio

  : Synthesizes preconditions of C# programs using a test generator as the verification oracle.

• Sorcar

  : Algorithm to learn conjunctive inductive invariants.

• NPI

  : Synthesizes inductive invariants using an incomplete verification oracle.

• Alchemist

  : A General-purpose SyGuS solver to synthesize CLIA expressions.
  Won second place in the 2015 SyGuS competition (CLIA track).

• NetGen

  : Synthesizes network data-plane configuration changes from high-level policy change specifications.

Teaching

• Formal Software Development Methods (CS477):

    Fall 2016
  University of Illinois at Urbana Champaign.

• Software Design Studio (CS126):

    Fall 2017, Spring 2018
  University of Illinois at Urbana Champaign.

• Data Visualization (CS498 DDV):

    Summer 2018
  Part of Data Mining Specialization at Coursera, offered by University of Illinois.

Talks

• Software Engineering Institute, CMU, 2023:

    Specification Mining.
  

• MathWorks, 2020:

    Program Synthesis.
  

• GE Research, 2020:

    Program Synthesis.
  

• Excape PI Meeting, 2017:

    Network Synthesis.
  

• Midwest Verification Week, 2015:

    Network Synthesis.
  

• CAV, 2015:

    Alchemist: Learning Guarded Affine Functions.
  

• SOSR, 2015:

    NetGen: Synthesizing Data-plane Configurations for Network Policies.
  

• Excape PI Meeting, 2015:

    NetGen: Synthesizing Data-plane Configurations for Network Policies.