diff --git a/_research/concurrency.md b/_research/concurrency.md index 0df63bbf98e20bab9aec6af35d72b51bff9ae4bb..1ee85df7dc91e86d8e1de4533d968ee7febaf311 100644 --- a/_research/concurrency.md +++ b/_research/concurrency.md @@ -7,7 +7,7 @@ Concurrent programs and libraries are ubiquitous in today's world of multi-core and the need for reasoning about concurrent programs and verifying their correctness grows increasingly more important. These research problems are still considered difficult for a variety of reasons, such as the fact that we need to consider and reach conclusions about a shared state -affected by multiple threads. +affected by multiple threads, or that we require effective abstractions for describing the complex behaviour created by multiple threads. Our research agenda is to develop formal reasoning methods about concurrency with a focus on concurrent program logics. Recently, various logics based on separation logic were introduced with the aim of verifying functional correctness of fine-grained concurrent programs.