diff --git a/_posts/2017-05-09-Kloss.md b/_posts/2017-05-09-Kloss.md index ea725d4694132012188ba4b3ff1604cf99572256..1fffa88eec15908b13e58d7e680e893c6bb0e946 100644 --- a/_posts/2017-05-09-Kloss.md +++ b/_posts/2017-05-09-Kloss.md @@ -4,7 +4,8 @@ title: Johannes Kloss, visitor from MPI [Johannes Kloss]( https://people.mpi-sws.org/~jkloos/), a fourth-year PhD student at the [Max Planck Institute for Software Systems](https://www.mpi-sws.org/) visited the group this week. -Johannes gave a talk to the group about his current research, on Reasoning about event-based concurrency with Asynchronous Liquid Separation Types +Johannes gave a talk to the group about his current research, on Reasoning about event-based concurrency with Asynchronous Liquid Separation Types. + The talk abstract: I will present work on a program logic and associated type system for reasoning about asynchronous programs manipulating shared mutable state. The logic and type system guarantee the absence of races and the preservation of user-specified invariants using a combination of two ideas: refinement types and concurrent separation logic. The logic track ownership of shared state across concurrently posted tasks and allow reasoning about