I am a PhD student in the Computer Science Department of New York University. I am interested in the fields of Formal Verification and Machine Learning. I am currently working with Thomas Wies on creating a proof framework for concurrent dictionary data structures. I have also worked on using Machine Learning for program verification and synthesis, and on using SMT and local theories to verify heap manipulating programs.
2013 –  NYU, Courant Institute of Mathematical Sciences, Ph.D. Computer Science 
2013 – 2015  NYU, Courant Institute of Mathematical Sciences, M.S. Computer Science 
2010 – 2013  Chennai Mathematical Institute, B.Sc. (Hons.) Mathematics and Computer Science 
firstname (at) cs(.)nyu(.)edu  
LinkedIn profile  
Room 405 NYU Computer Science 60 Fifth Avenue New York, NY 10011 
Learning Shape Analysis Marc Brockschmidt, Yuxin Chen, Byron Cook, Pushmeet Kohli, Siddharth Krishna, Daniel Tarlow, and He ZhuStatic Analysis Symposium (SAS 2017)Earlier version: Learning to Verify the Heap (Microsoft Tech Report)See abstractWe present a datadriven verification framework to automatically prove memory safety of heapmanipulating programs. Our core contribution is a novel statistical machine learning technique that maps observed program states to (possibly disjunctive) separation logic formulas describing the invariant shape of (possibly nested) data structures at relevant program locations. We then attempt to verify these predictions using a program verifier, where counterexamples to a predicted invariant are used as additional input to the shape predictor in a refinement loop. We have implemented our techniques in Locust, an extension of the GRASShopper verification tool. Locust is able to automatically prove memory safety of implementations of a variety of classical heapmanipulating programs such as insertionsort, quicksort and traversals of nested data structures. 
Learning Invariants using Decision Trees Siddharth Krishna, Christian Puhrsch and Thomas WiesTechnical report, arXiv. (PDF) January, 2015See abstractThe problem of inferring an inductive invariant for verifying program safety can be formulated in terms of binary classification. This is a standard problem in machine learning: given a sample of good and bad points, one is asked to find a classifier that generalizes from the sample and separates the two sets. Here, the good points are the reachable states of the program, and the bad points are those that reach a safety property violation. Thus, a learned classifier is a candidate invariant. In this paper, we propose a new algorithm that uses decision trees to learn candidate invariants in the form of arbitrary Boolean combinations of numerical inequalities. We have used our algorithm to verify C programs taken from the literature. The algorithm is able to infer safe invariants for a range of challenging benchmarks and compares favorably to other MLbased invariant inference techniques. In particular, it scales well to large sample sets. I have presented this work at FMCAD's student forum (October 2014). Here is my poster. My poster on this work also won second place at POPL's student poster competition (January 2015). 
A quadratic construction for Zielonka automata with acyclic communication structure Siddharth Krishna and Anca MuschollTheoretical Computer Science September 9, 2013See abstractAsynchronous automata are parallel compositions of finitestate processes synchronizing over shared variables. A deep theorem due to Zielonka says that every regular trace language can be recognized by a deterministic asynchronous automaton. The construction is rather involved and the most efficient variant produces automata which are exponential in the number of processes and polynomial in the size of the DFA. In this paper we show a simple, quadratic construction in the case where the synchronization actions are binary and define an acyclic communication graph.

"Learning to Verify the Heap" at EPFL, Lausanne and UCL, London Jun 2016 (PDF) 
"Learning to Verify the Heap" at Yale PL Day, Yale University, USA Nov 2015 
Henning Biermann Award 2015Received award from NYU CS department for exceptional contributions to education and service. 
Dr S Parthasarathy Award for Undergraduate Research 2013Received award on graduating from CMI for original research during undergraduate studies. 
ACM Inter Collegiate Programming Contest 2011, 2012Was part of a three member team that qualified twice for the World Finals. We came 1st in 2011 and 2nd in 2012 in the regionals. 
International Olympiad in Informatics Aug ’10Represented India in the international round (was one of 4 member team), and won an individual Bronze medal. 
Rhodes Scholarship Finalist Nov ’12Was one of the 18 students from India across all disciplines shortlisted for the Rhodes Scholarship. 
KVPY Fellowship Apr ’10Was one of the 20 students from across India to be awarded the prestigious science fellowship (KVPY) for a Mathematics project titled “Rational Approximations to the roots of x^x”. 
Research Intern June 2016 – August 2016 (3 months)Microsoft Research, CambridgeWorked with Marc Brockschmidt and Daniel Tarlow on learning generative models of source code with applications to program synthesis. 
Research Intern May 2015 – August 2015 (3 months)Microsoft Research, CambridgeWorked with Marc Brockschmidt and Daniel Tarlow on using Machine Learning to verify heap manipulating programs. 
Engineering Intern May 2014 – July 2014 (3 months)Quora, Mountain ViewDeveloped the infrastructure and machine learning used to find and rank related questions within Quora's knowledge base. Used Python, C++, Redshift and Hive. 
Research Intern May 2013 – July 2013 (3 months)LSV, ENS de Cachan, ParisWorked with Paul Gastin on Multiple Context Free Grammars and connections to Push Down Automata. 
Research Intern May 2012 – July 2012 (3 months)LaBRI, Universite Bordeaux, FranceWorked with Anca Muscholl and Hugo Gimbert.

Research Intern May 2011 – July 2011 (3 months)The Institute of Mathematical Sciences, ChennaiWith R. Shankar, on a project to model glacier dynamics. Used Python to analyse geological survey data and find errors. 
Coach June 2011 – June 2011 (1 month)International Olympiad in Informatics (IOI) Training Camp, India. 
Programming Intern May 2010 – June 2010 (2 months)Strand Life Sciences 