diff --git a/_posts/2020-06-16-advert.md b/_posts/2020-06-16-advert.md index 803656b107a21470c8499e998ca440be64794a80..5451a78ed107ba0cda77905f343f382788799eb5 100644 --- a/_posts/2020-06-16-advert.md +++ b/_posts/2020-06-16-advert.md @@ -25,8 +25,7 @@ who fund part of the group's research. Several potential projects are listed below, focussing on symbolic analysis, concurrency and distribution. -#### Gillian: a multi-language platform for compositional symbolic -analysis +### Gillian: a multi-language platform for compositional symbolic analysis The Verified Software Group has recently introduced [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html) (PLDI'20), @@ -41,7 +40,7 @@ There are many possible projects. We would especially like to recruit someone interested in extending Gillian with concurrency or underpinning Gillian with Coq-certification. -#### Concurrency +### Concurrency The Verified Software Group has worked on compositional reasoning about concurrent programs, introducing fundamental techniques underpinning modern @@ -56,7 +55,7 @@ fundamental theory; applying the work to real-world libraries; developing prototype analysis tools; or moving to the Coq-focused Iris project, which uses much of our foundational theory. -#### Distribution. +### Distribution The Verified Software Group recently began to work on weak consistency models for distribution, developing an interleaving operational semantics for