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
126 commits behind the upstream repository.
2021-07-01-toplas.md 1.83 KB 1.23 KiB 
---
title: Paper accepted at TOPLAS
---

Many congratulations to [Emanuele D’Osualdo](https://www.emanueledosualdo.com/about/), [Azadeh Farzan](https://www.cs.toronto.edu/~azadeh/), Philippa Gardner and [Julian Sutherland](https://www.doc.ic.ac.uk/~jhs110/), whose paper [“TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs”](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications/-/blob/d7c1f1ee5690694acefb7f8836dda455ae309b05/DOsualdo2020TaDa.pdf) has been accepted for publication at the [ACM Transactions on Programming Languages and Systems (TOPLAS)](https://dl.acm.org/journal/toplas) journal. 

The paper introduces TaDA Live, a separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The logic contributes several innovations to obtain modular rely/guarantee style reasoning for liveness properties and to blend them with logical atomicity.  

TOPLAS is the bimonthly ACM peer-reviewed scientific journal on programming languages. TOPLAS reports in depth on recent research advances in the areas of programming languages. Papers published must have content that is innovative, novel and advances the art of programming languages and systems.