From 863eb8ed679f500791d3204d2a4633d33cc8f4bf Mon Sep 17 00:00:00 2001 From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk> Date: Fri, 24 Nov 2017 12:19:55 +0000 Subject: [PATCH] Update 2017-11-24-siddharth.md --- _posts/2017-11-24-siddharth.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/_posts/2017-11-24-siddharth.md b/_posts/2017-11-24-siddharth.md index bc66431..74c7a9f 100644 --- a/_posts/2017-11-24-siddharth.md +++ b/_posts/2017-11-24-siddharth.md @@ -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. 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). +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](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, 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 -- GitLab