@@ -5,10 +5,13 @@ We are very pleased to have welcome [Siddharth Krishna](https://cs.nyu.edu/~sidd
...
@@ -5,10 +5,13 @@ We are very pleased to have welcome [Siddharth Krishna](https://cs.nyu.edu/~sidd
who visited the group this week to talk about his work on the verification of concurrent data structures.
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
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
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).
for Concurrent Data Structures](https://cs.nyu.edu/~siddharth/pubs/2018-popl-flows.pdf), joint work with Dennis Shasha and Thomas Wies, to appear
at [POPL 2018](https://popl18.sigplan.org/home).
The abstract of the talk is: Concurrent separation logics have helped to significantly simplify correctness proofs for concurrent data structures.
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,
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
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
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
