Concurrent programs and libraries are ubiquitous in today's world of multi-core processor architectures.
Reasoning about concurrent programs and verifying their correctness is increasingly important.
However, reasoning about concurrent programs is a difficult problem.
We have to take shared state that is being changed by multiple threads into account.
Concurrent programs and libraries are ubiquitous in today's world of multi-core processor architectures,
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, or [another reason].
Our research agenda is to develop formal reasoning methods about concurrency with a focus on concurrent program logics.
Recently, there have been various logics based on separation logic to verify functional correctness of fine-grained concurrent programs.
We have played a significant role introducing {% cite_details Dinsdale-Young2010Concurrent --text Concurrent Abstract Predicates %}, {% cite_details Dinsdale-Young2013Views --text Views %}, {% cite_details daRochaPinto2014TaDA --text TaDA %}, {% cite_details Raad2015CoLoSL --text CoLoSL %}, {% cite_details Ntzik2015Fault --text Fault-tolerant Concurrent Separation Logic %} and {% cite_details daRochaPinto2016Modular --text Total-TaDA %}.
These logics have tackled a range of problems, ranging data abstraction, atomicity abstraction, fault-tolerance, terminal, as well as introducing more modular and compositional ways to reason about concurrent programs.
We have applied these logics to verify large problems, such as data structures used in databases and java.util.concurrent, as well as specifying file systems.
Recently, various logics based on separation logic were introduced with the aim of verifying functional correctness of fine-grained concurrent programs.
We have played a significant role in the development of {% cite_details Dinsdale-Young2010Concurrent --text Concurrent Abstract Predicates %}, {% cite_details Dinsdale-Young2013Views --text Views %}, {% cite_details daRochaPinto2014TaDA --text TaDA %}, {% cite_details Raad2015CoLoSL --text CoLoSL %}, {% cite_details Ntzik2015Fault --text Fault-tolerant Concurrent Separation Logic %} and {% cite_details daRochaPinto2016Modular --text Total-TaDA %}.
These logics have tackled a range of problems, including data abstraction, atomicity abstraction, fault-tolerance, terminal, while introducing more modular and compositional ways to reason about concurrent programs.
We have applied these logics to the verification of large problems, such as data structures used in databases and java.util.concurrent, as well as the specification of file systems.
We aim to continue improving the state-of-the-art with a focus on progress properties, specifying concurrency in POSIX filesystems, continuing improving our logics to tackle more advanced algorithms, and develop automated reasoning tools based on these logics.
Our mission is to continually challenge and improve the state-of-the-art, targeting progress properties, specification of concurrency in POSIX filesystems, refinement of our logics so that we are able to deal with more advanced algorithms, and the development of automated reasoning tools based on these logics.
