Siddharth Krishna

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 the verification of concurrent 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.

Profile picture


2013 –NYU, Courant Institute of Mathematical Sciences,
Ph.D. Computer Science
2013 – 2015NYU, Courant Institute of Mathematical Sciences,
M.S. Computer Science
2010 – 2013Chennai Mathematical Institute,
B.Sc. (Hons.) Mathematics and Computer Science


siddharth (at)
LinkedIn profile
Room 418,
NYU Computer Science,
60 Fifth Avenue,
New York, NY 10011.


Verifying Concurrent Search Structure Templates
Siddharth Krishna, Dennis Shasha, and Thomas Wies

Under review April 2019

See abstract

Concurrent separation logics have had great success reasoning about concurrent data structures. This success stems from their application of modularity on multiple levels, leading to proofs that are decomposed according to program structure, program state, and individual threads. Despite these advances, it remains difficult to achieve proof reuse across different data structure implementations. For the large class of search structures, we demonstrate how one can achieve further proof modularity by decoupling the proof of thread safety from the proof of structural integrity. We base our work on the template algorithms of Shasha and Goodman that dictate how threads interact but abstract from the concrete layout of nodes in memory. Building on the recently proposed flow framework of compositional abstractions and the separation logic Iris, we show how to prove correctness of template algorithms, and how to instantiate them to obtain multiple verified implementations.

We demonstrate our approach by formalizing three concurrent search structure templates, based on link, give-up, and lock-coupling synchronization, and deriving verified implementations based on B-trees, hash tables, and linked lists. These case studies represent algorithms used in real-world file systems and databases, which have so far been beyond the capability of automated or mechanized state-of-the-art verification techniques. Our verification is split between the Coq proof assistant and the deductive verification tool GRASShopper in order to demonstrate that our proof technique and framework can be applied both in fully mechanized proof assistants as well as automated program verifiers. In addition, our approach reduces proof complexity and is able to achieve significant proof reuse.

Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Siddharth Krishna, Dennis Shasha, and Thomas Wies

Proceedings of the ACM on Programming Languages (POPL 2018) January 2018

See abstract
Concurrent separation logics have helped to significantly simplify correctness proofs for concurrent data structures. However, a recurring problem in such proofs is that data structure abstractions that work well in the sequential setting are much harder to reason about in a concurrent setting due to complex sharing and overlays. To solve this problem, we propose a novel approach to abstracting regions in the heap by encoding the data structure invariant into a local condition on each individual node. This condition may depend on a quantity associated with the node that is computed as a fixpoint over the entire heap graph. We refer to this quantity as a flow. Flows can encode both structural properties of the heap (e.g. the reachable nodes from the root form a tree) as well as data invariants (e.g. sortedness). We then introduce the notion of a flow interface, which expresses the relies and guarantees that a heap region imposes on its context to maintain the local flow invariant with respect to the global heap. Our main technical result is that this notion leads to a new semantic model of separation logic. In this model, flow interfaces provide a general abstraction mechanism for describing complex data structures. This abstraction mechanism admits proof rules that generalize over a wide variety of data structures. To demonstrate the versatility of our approach, we show how to extend the logic RGSep with flow interfaces. We have used this new logic to prove linearizability and memory safety of nontrivial concurrent data structures. In particular, we obtain parametric linearizability proofs for concurrent dictionary algorithms that abstract from the details of the underlying data structure representation. These proofs cannot be easily expressed using the abstraction mechanisms provided by existing separation logics.

Learning Shape Analysis
Marc Brockschmidt, Yuxin Chen, Pushmeet Kohli, Siddharth Krishna, and Daniel Tarlow

Static Analysis Symposium (SAS 2017) August 2017

Earlier version: Learning to Verify the Heap (Microsoft Tech Report)

See abstract

We present a data-driven verification framework to automatically prove memory safety of heap-manipulating 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 heap-manipulating programs such as insertionsort, quicksort and traversals of nested data structures.

Learning Invariants using Decision Trees
Siddharth Krishna, Christian Puhrsch and Thomas Wies

Technical report, arXiv. January, 2015

See abstract

The 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 ML-based 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 Muscholl

Theoretical Computer Science September 9, 2013

See abstract
Asynchronous automata are parallel compositions of finite-state 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.


"Automating the Flow Framework" at ADSL 2018

"Go with the Flow: Compositional Abstractions for Concurrent Data Structures" at POPL 2018

"Flow Interfaces" at IBM PL Day Dec 2017

"Flow Interfaces" at Leicester Univeristy (Slides) and Imperial College (Slides) Nov 2017

"Learning to Verify the Heap" at EPFL, Lausanne and UCL, London Jun 2016 (Slides)

"Learning to Verify the Heap" at Yale PL Day, Yale University Nov 2015

"Implementing distributed control on star architectures" at GAMES 2012 Sep 2012


Program Committee member FTfJP 2018

External reviewer OOPSLA 2018

Subreviewer TACAS 2018, VMCAI 2018, SAS 2017, CONCUR 2017, ESOP 2017, ESOP 2016, FMCAD 2015, CADE-25, TACAS 2015

Awards & Honours

Dean's Dissertation Fellowship 2018

A 1 year fellowship given to 30 PhD students from across NYU's Graduate School of Arts and Science.

Henning Biermann Award 2015

An award from NYU CS department for exceptional contributions to education and service.

Dr S Parthasarathy Award for Undergraduate Research 2013

An award from CMI for original research during undergraduate studies.

ACM Inter Collegiate Programming Contest 2011, 2012

Was 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 ’10

Represented India in the international round (was one of 4 member team), and won an individual Bronze medal.


Fundamental Algorithms (graduate) NYU, Fall 2017

I was the Teaching Assistant (Recitation Leader). Recitation homepage.

Data Structures (undergraduate) NYU, Spring 2016

I was the Teaching Assistant (Recitation Leader). Recitation homepage.


Research Intern August 2018 – November 2018

SRI International, New York

Worked with Michael Emmi on correctness of concurrent libraries.

Research Intern June 2016 – August 2016 (3 months)

Microsoft Research, Cambridge

Worked 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, Cambridge

Worked 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 View

Developed 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, Paris

Worked 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, France

Worked with Anca Muscholl and Hugo Gimbert on the synthesis of controllers for distributed systems.