From a4cd16713547d215dce3164e6aa8594bddecbc5d Mon Sep 17 00:00:00 2001
From: Thomas Wood <thomas.wood09@imperial.ac.uk>
Date: Thu, 4 Feb 2016 16:51:44 +0000
Subject: [PATCH] Add concurrency research page
---
Gemfile.lock | 2 +-
assets/blog.scss | 4 ++++
publications/publications.bib | 4 +++-
research/concurrency.md | 24 ++++++++++++++++++++++++
4 files changed, 32 insertions(+), 2 deletions(-)
create mode 100644 research/concurrency.md
diff --git a/Gemfile.lock b/Gemfile.lock
index 428ce62..e19d688 100644
--- a/Gemfile.lock
+++ b/Gemfile.lock
@@ -1,6 +1,6 @@
GIT
remote: https://github.com/edgemaster/jekyll-scholar.git
- revision: b35ce69e6901c8f3cd46455fb600e285ea0977f4
+ revision: 867c1f71c4a0f76e08cceb2b2a012243c83ecceb
branch: master
specs:
jekyll-scholar (5.7.0)
diff --git a/assets/blog.scss b/assets/blog.scss
index 87bbc2f..d24b2d1 100644
--- a/assets/blog.scss
+++ b/assets/blog.scss
@@ -265,3 +265,7 @@ h6, .h6 {
.people {
min-height: 280px;
}
+
+.post-content {
+ text-align: justify;
+}
diff --git a/publications/publications.bib b/publications/publications.bib
index 078a5f7..1b03715 100644
--- a/publications/publications.bib
+++ b/publications/publications.bib
@@ -535,7 +535,9 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
Month = {April},
Pages = {207--231},
- Abstract = {We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread's concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.}
+ Abstract = {We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread's concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.},
+
+ Project = { concurrency, tada }
}
@InProceedings{Wischik2004Strong,
diff --git a/research/concurrency.md b/research/concurrency.md
new file mode 100644
index 0000000..09ff838
--- /dev/null
+++ b/research/concurrency.md
@@ -0,0 +1,24 @@
+---
+title: Concurrency
+menu:
+menu_order: 1
+---
+
+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, 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.
+
+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 can deal with more advanced algorithms, and the development of automated reasoning tools based on these logics.
+
+Recent Publications
+===================
+
+{% bibliography -q @*[project ~= concurrency] --max 5 %}
--
GitLab