@@ -4,7 +4,8 @@ title: Johannes Kloss, visitor from MPI
...
@@ -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/)
[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.
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
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:
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
refinement types and concurrent separation logic. The logic track ownership of shared state across concurrently posted tasks and allow reasoning about
