Shambwaditya
Saha

Research Interests

• Natural Language Processing, Deep Learning, Program Synthesis, Program Verification, Formal Methods.

Employment

• Personal Sabbatical:

  
  September 2021 to December 2022.

• Tufts University: Postdoctoral Researcher, under Prof. Jeff Foster

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

• Runtime Verification: Research Internship

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

Education

• Integrated Ph.D., Computer Science

  
  University of Illinois at Urbana-Champaign, December 2019
  

• Master of Science, Computer Science

  
  Chennai Mathematical Institute, India, August 2011
  GPA: 3.62 / 4

Publications

• Synthesizing Contracts Correct Modulo a Test Generator

    PDF
  with Angello Astorga, 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
  with Daniel Neider, P. Madhusudan, Pranav Garg, Daejun Park
  Journal of Automated Reasoning (JAR), 2020. Invited Article

• Learning Stateful Preconditions Modulo a Test Generator

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

• Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants

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

• Compositional Synthesis of Piece-Wise Functions by Learning Classifiers

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

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

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

• Invariant Synthesis for Incomplete Verification Engines

    PDF
  with Daniel Neider, Pranav Garg, P. Madhusudan, 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
  with Daniel Neider, P. Madhusudan
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016.

• Alchemist: Learning Guarded Affine Functions

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

• NetGen: Synthesizing Data-plane Configurations for Network Policies

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

• Syntax-Guided Synthesis

    PDF
  with Rajeev Alur, Rastislav Bodik, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas KressGazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, 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

• 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.