From 647d0d20576bd936f16044411fc3ab054f78653c Mon Sep 17 00:00:00 2001
From: Gian Ntzik <gian.ntzik08@imperial.ac.uk>
Date: Wed, 3 Feb 2016 20:51:38 +0000
Subject: [PATCH] Updated blurb on concurrency

---
 index.md | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/index.md b/index.md
index 49011a2..6bf3749 100644
--- a/index.md
+++ b/index.md
@@ -4,4 +4,14 @@ menu: true
 menu_order: 1
 ---
 
-[BLURB ON CONCURRENCY]
+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.
+
+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 Concurrent Abstract Predicates, the Views framework, TaDA, CoLoSL, Fault-tolerant Concurrent Separation Logic and 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.
+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.
-- 
GitLab