Skip to content
Snippets Groups Projects
Select Git revision
  • master default
  • fix-bibtex-unicode-filter
  • dataspy-hacking
3 results
Blame Permalink
Forked from Verified Software / psvg.doc.ic.ac.uk
257 commits behind the upstream repository.
concurrency.md 1.77 KiB 
title: Concurrency
project_id: concurrency
menu: true
parent_menu: Research
menu_order: 4
sub_menu_order: 1

We develop compositional reasoning techniques for concurrent programs using modern concurrent separation logics, introducing fundamental concepts in the reasoning: logical abstraction (Concurrent Abstract Predicates), logical atomicity (the TaDA Logic) and logical environment liveness properties (TaDA Live). In addition, we have started to work on weak consistency models for distribution, developing an interleaving operational semantics for client-observational behaviour of atomic transactions (ECOOP’20).

We have applied our reasoning to, for example, algorithms for manipulating concurrent B-trees, skip lists from java.util.concurrent, graph algorithms and the POSIX file system. Our goal is to challenge and improve the state-of-the-art in concurrent reasoning, refining our logics to deal with more advanced concurrent programs, developing automated reasoning tools based on these logics, and applying our work to real-world concurrent programs.

Research Support

This research is supported by Gardner's UKRI Established Career Fellowship ["VeTSpec: Verified Trustworthy Software Specification"][VeTSpec] and Emanuele D'Osualdo's Marie-Curie Fellowship "VeSPA: Verification through Security and Progress Abstractions". It was previously supported by the EPSRC programme grant EP/K008528/1: REMS: Rigorous Engineering of Mainstream Systems and the EPSRC programme grant EP/H008373/2: Resource Reasoning.