diff --git a/_posts/2017-11-24-siddharth.md b/_posts/2017-11-24-siddharth.md
new file mode 100644
index 0000000000000000000000000000000000000000..e966264c13b685b4465c5b81bc546296a190187a
--- /dev/null
+++ b/_posts/2017-11-24-siddharth.md
@@ -0,0 +1,23 @@
+---
+title: Visitor to the group, Siddharth Krishna, New York University, USA
+---
+We are very pleased to have welcome [Siddharth Krishna](https://cs.nyu.edu/~siddharth/), from the Courant Institute of Mathematical Sciences, NYU, 
+who visited the group this week to talk about his work on the verification of concurrent data structures.
+
+Siddharth is a PhD student in the Computer Science Department of New York University, working on Formal Verification and Machine Learning under the supervision 
+of [Thomas Wies](https://cs.nyu.edu/wies/). Siddharth gave a talk based on his forthcoming paper on Flow Interfaces: Go with the Flow: Compositional Abstractions 
+for Concurrent Data Structures, joint work with Dennis Shasha and Thomas Wies, to appear at [POPL 2018](https://cs.nyu.edu/~siddharth/pubs/2018-popl-flows.pdf).
+
+The abstract of the talk is: 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, such as inductive predicates, 
+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.
\ No newline at end of file