_posts/2016-09-01-newmember.md

 ---
 title: Welcome to Andrea Cerone, new member of the group
 ---
-We are very happy to welcome Andrea Cerone to the group. Andrea has joined us from the [IMDEA Software Institute](http://software.imdea.org/about.html), Madrid, Spain, where he worked with Dr. Alexey Gotsman on Verification of Higher Order Concurrent Libraries and Foundations of Consistency Models for Distributed Databases. 
+We are very happy to welcome Andrea Cerone to the group. Andrea has joined us from the [IMDEA Software Institute](http://software.imdea.org/about.html), Madrid, Spain, 
+where he worked with Dr. Alexey Gotsman on Verification of Higher Order Concurrent Libraries and Foundations of Consistency Models for Distributed Databases. 
 
-Andrea is currently working on frameworks for specifying weak consistency models of geo-replicated databases and applications of transaction chopping for various consistency models. Andrea did his Ph.D at Trinity College Dublin with Prof Matthew Hennessy, so he claims to be quite unfazed by the UK weather.
+Andrea is currently working on frameworks for specifying weak consistency models of geo-replicated databases and applications of transaction 
+chopping for various consistency models. Andrea did his Ph.D at Trinity College Dublin with Prof Matthew Hennessy, so he claims to be quite unfazed by the UK weather.
 
-You can find more about Andrea on [his webpage](https://www.doc.ic.ac.uk/~acerone/)
+You can find more about Andrea on [his webpage](https://www.doc.ic.ac.uk/~acerone/).
 
 

_posts/2016-10-03-papers.md

@@ -3,5 +3,6 @@ title: Papers published by Azalea Raad
 ---
 Azalea Raad has had two papers published in Programming Languages and System: Proceedings of the 14th Asian Symposium, [APLAS 2016](https://soict.hust.edu.vn/~aplas2016/).
 
-The papers are: [Verifying Concurrent Graph Algorithms](http://psvg.doc.ic.ac.uk/publications/Raad2016Verifying.html) (with Aquinas Hobor, Jules Villard and Philippa Gardner) and [DOM: Specification and Client Reasoning](http://psvg.doc.ic.ac.uk/publications/Raad2016DOM.html) (with José Fragoso Santos and Philippa Gardner)
-These and other group papers can be found on our [publications page](http://psvg.doc.ic.ac.uk/publications/)
+The papers are: [Verifying Concurrent Graph Algorithms](http://vtss.doc.ic.ac.uk/publications/Raad2016Verifying.html) (with Aquinas Hobor, Jules Villard and Philippa Gardner) and [DOM: Specification and Client Reasoning](http://vtss.doc.ic.ac.uk/publications/Raad2016DOM.html) (with José Fragoso Santos and Philippa Gardner).
+
+These and other group papers can be found on our [publications page](http://vtss.doc.ic.ac.uk/publications/).

_posts/2016-11-14-inferlab.md

@@ -2,7 +2,7 @@
 title: Infer Lab at Imperial
 ---
 
-The [Separation Logic](https://psvg.doc.ic.ac.uk/teaching/separationlogic.html) course team ran a lab on [Infer](http://fbinfer.com/), 
+The [Separation Logic]({{site.baseurl}}{% link teaching/separationlogic.md %}) course team ran a lab on [Infer](http://fbinfer.com/), 
 an automatic verification tool based on separation logic, developed at [Facebook](https://www.facebook.com/inferstaticanalyzer/) 
 where it is used every day to verify millions of lines of code.
 
@@ -19,4 +19,4 @@ During the tutorial, one of the students, Lorenzo Paoliani, ran Infer on Connect
 and found several null dereference bugs. He reported this on github and submitted a pull request for fixing that problem, 
 which has been accepted and now merged.
 
-For more details and slides, see the [Infer Lab 2016](https://psvg.doc.ic.ac.uk/teaching/InferLab.html) page.
\ No newline at end of file
+For more details and slides, see the [Infer Lab 2016]({{site.baseurl}}{% link teaching/InferLab.md %}) page.
\ No newline at end of file

_posts/2016-11-23-dagstuhl.md

@@ -8,4 +8,4 @@ Andrea Cerone was invited to attend the seminar on [Concurrency with Weak Memory
 
 The seminar covered a wide range of topics, including fundamental results in the theory underlying weak memory models, 
 applications in the fields of hardware architectures, compiler optimisations and transactional systems, 
-as well as static analysis techniques for the analysis of programs. Andrea Cerone gave a talk on ‘Analyzing Snapshot Isolation’
+as well as static analysis techniques for the analysis of programs. Andrea Cerone gave a talk on 'Analyzing Snapshot Isolation'.

_posts/2016-12-15-Dolby.md

@@ -3,10 +3,12 @@ title: Visit from Julian Dolby, IBM
 ---
 [Julian Dolby](http://researcher.watson.ibm.com/researcher/view.php?person=us-dolby), a researcher at IBM's 
 [Thomas J. Watson Research Center](http://www.research.ibm.com/labs/watson/index.shtml)
-in New York visited the PSVG group for a week in December. Julian’s research focuses on static program analysis, 
+in New York visited the VTSS group for a week in December.
+
+Julian’s research focuses on static program analysis, 
 software testing and the semantic web and during his visit, Julian worked with José Fragoso and Petar Maksimovic 
-in a [symbolic analysis for JavaScript](https://psvg.doc.ic.ac.uk/research/javascript.html) 
+in a [symbolic analysis for JavaScript]({{site.baseurl}}{% link research/javascript.md %}) 
 based on JSIL and Rosette with the end goal of having a bug-finding tool for JavaScript.
 
 [ROSETTE](https://github.com/juliandolby/rosette) is a solver-aided programming language 
-that extends Racket with language constructs for program synthesis, verification, and more.
\ No newline at end of file
+that extends Racket with language constructs for program synthesis, verification, and more.

_posts/2017-01-13-Pedro_viva.md

@@ -2,12 +2,14 @@
 title: Successful viva for Pedro da Rocha Pinto
 ---
 
-Congratulations to Pedro da Rocha Pinto who defended his PhD thesis, Reasoning with Time and Data Abstractions at his viva on Friday 13th January 2017.  
+Congratulations to Pedro da Rocha Pinto who defended his PhD thesis, Reasoning with Time and Data Abstractions at his viva on Friday 13th January 2017. 
+
 The viva was passed with minor corrections. Many thanks to [Aleksandar Nanevski](http://software.imdea.org/~aleks/) 
 and [Viktor Vafeiadis]( https://people.mpi-sws.org/~viktor/) who acted as external examiner 
 and to [Susan Eisenbach](http://www.imperial.ac.uk/people/s.eisenbach), who acted as the internal examiner.
 
 Pedro’s thesis was about exploring a number of design possibilities for a logic for 
 modularly verifying shared-memory concurrent programs and introduces a new program logic 
-called [TaDA](https://psvg.doc.ic.ac.uk/publications/daRochaPinto2014TaDA.html) for verifying concurrent programs with much better support for abstraction 
-The latest paper from Pedro, accepted to ESOP 2017 is on [our publications page](https://psvg.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html)
+called [TaDA]({{site.baseurl}}{% link publications/daRochaPinto2014TaDA.html %}) for verifying concurrent programs with much better support for abstraction.
+
+Pedro's latest paper, accepted to ESOP 2017 is on [our publications page]({{site.baseurl}}{% link publications/Dinsdale-Young2017Caper.html %}).

_posts/2017-02-01-Gian_viva.md

@@ -12,4 +12,4 @@ clients that interact with the API. The examiners found that Gian’s work conta
 on formal specification and verifications of concurrent software systems and recommended 
 that the viva is passed with only minor corrections. 
 
-More details on Gian’s research can be found [here](https://psvg.doc.ic.ac.uk/people/ntzik.html)
+More details on Gian’s research can be found [here]({{site.baseurl}}{% link _people/ntzik.md %}).

_posts/2017-02-06-ESOP.md

@@ -3,17 +3,17 @@ title: Papers accepted at ESOP 2017
 ---
 
 Two papers from the concurrency project team have been accepted at 26th European Symposium on Programming [(ESOP 2017)](http://www.etaps.org/index.php/2017/esop),
-which will take place this April in Uppsala, Sweden. The first paper, [Abstract Specifications for Concurrent Maps](https://psvg.doc.ic.ac.uk/publications/Xiong2017Abstract.html), present the importance of abstract atomicity for reasoning fine-grained concurrent modules.
-The second paper, [Caper: Automatic Verification for Fine-grained Concurrency](https://psvg.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html), presents a prototype tool for automated reasoning about concurrent modules. 
+which will take place this April in Uppsala, Sweden. The first paper, [Abstract Specifications for Concurrent Maps]({{site.baseurl}}{% link publications/Xiong2017Abstract.html %}), present the importance of abstract atomicity for reasoning fine-grained concurrent modules.
+The second paper, [Caper: Automatic Verification for Fine-grained Concurrency]({{site.baseurl}}{% link publications/Dinsdale-Young2017Caper.html %}), presents a prototype tool for automated reasoning about concurrent modules. 
 
-The first paper, submitted by [Shale Xiong](https://psvg.doc.ic.ac.uk/people/xiong.html), [Pedro Da Rocha Pinto](https://psvg.doc.ic.ac.uk/people/da-rocha-pinto.html), 
-[Gian Ntzik](https://psvg.doc.ic.ac.uk/people/ntzik.html) and [Philippa Gardner](https://psvg.doc.ic.ac.uk/people/gardner.html),
-[Abstract Specifications for Concurrent Maps](https://psvg.doc.ic.ac.uk/publications/Xiong2017Abstract.html) demonstrates that abstract atomicity 
+The first paper, submitted by [Shale Xiong](https://vtss.doc.ic.ac.uk/people/xiong.html), [Pedro Da Rocha Pinto]({{site.baseurl}}{% link _people/da-rocha-pinto.md %}), 
+[Gian Ntzik](https://vtss.doc.ic.ac.uk/people/ntzik.html) and [Philippa Gardner]({{site.baseurl}}{% link _people/gardner.md %}),
+[Abstract Specifications for Concurrent Maps]({{site.baseurl}}{% link publications/Xiong2017Abstract.html %}) demonstrates that abstract atomicity 
 is key to give a specification for concurrent map that allows better client reasoning.
 This paper also provides the first functional correctness proof of ConcurrentSkiplistMap in java.util.concurrent with respect to the abstract specification.
 
 The second paper accepted, submitted by Pedro Da Rocha Pinto, in collaboration with [Thomas Dinsdale-Young](http://cs.au.dk/~tyoung/), 
 [Kristoffer Just Andersen](http://pure.au.dk/portal/en/persons/id(5e842a19-8b76-487a-8082-06b6d6ff2545).html)
-and [Lars Birkedal](http://www.cs.au.dk/~birke/) from Aarhus University is [Caper: Automatic Verification for Fine-grained Concurrency](https://psvg.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html).
+and [Lars Birkedal](http://www.cs.au.dk/~birke/) from Aarhus University is [Caper: Automatic Verification for Fine-grained Concurrency]({{site.baseurl}}{% link publications/Dinsdale-Young2017Caper.html %}).
 The paper presents [Caper](https://github.com/caper-tool/caper), a prototype tool for automated reasoning about concurrent modules.
 Caper is based on symbolic execution, integrating reasoning about interference on shared resources. This enables Caper to verify the functional correctness of fine-grained concurrent modules.

_posts/2017-02-11-INVEST.md

@@ -13,8 +13,8 @@ look at the fields of [software verification and testing](http://wp.doc.ic.ac.uk
 
 During the all day workshop, students were able to listen to and engage with world-leading academic 
 scholars, experience what it is like being a Verification and Testing researcher, and network with other students and current Post-Docs. 
-There were a number of talks, including one on How to Give Talks That People Can Follow, 
+There were a number of talks, including one on "How to Give Talks That People Can Follow",
 by [Derek Dreyer](https://people.mpi-sws.org/~dreyer/), of the [Max Planck Institute for 
 Software Systems (MPI-SWS), Germany]( https://www.mpi-sws.org/) and one minute presentations by students.
 
-![Derek Dreyer presenting his talk on How to Give Talks](/images/posts/Derek-Dreyer-talk-at-Invest-2017-4.jpg)
\ No newline at end of file
+![Derek Dreyer presenting his talk on How to Give Talks](/images/posts/Derek-Dreyer-talk-at-Invest-2017-4.jpg)

_posts/2017-02-14-NCSC_official_opening.md

 ---
 title: National Cyber Security Centre (NCSC) official opening
 ---
-Philippa Gardner attended the official opening by the Queen of the [National Cyber Security Centre](https://www.ncsc.gov.uk/) new headquarters in London. 
+Philippa Gardner attended the official opening by the Queen of the [National Cyber Security Centre](https://www.ncsc.gov.uk/)'s new headquarters in London.
 The NCSC, part of GCHQ, aims to make their work on cyber security more open; it will publish research, organise events and will provide advice 
 on cyber security to businesses and members of the public.
 
 Philippa was introduced to the Queen and spoke to her and Prince Philip about her role as director of the new Research Institute on Verified Trustworthy Software Systems (VeTSS).
 
-For details of the opening and a photo of the Queen see the [BBC news page on the opening](http://www.bbc.co.uk/news/uk-38964996)
+For details of the opening and a photo of the Queen see the [BBC news page on the opening](http://www.bbc.co.uk/news/uk-38964996).
 
-You can also check the [NCSC blog](https://www.ncsc.gov.uk/blog-post/how-ncsc-built-its-own-it-system) for details on how they built  their IT system.   
+You can also check the [NCSC blog](https://www.ncsc.gov.uk/blog-post/how-ncsc-built-its-own-it-system) for details on how they built their IT system.
 
 
 

_posts/2017-03-28-Colloquium.md

 ---
-title: Talk at Université Pierre et Marie Curie, Paris
+title: Philippa Gardner, invited speaker at Colloquium d'Informatique, Université Pierre et Marie Curie, Paris
 ---
 Philippa Gardner was the invited speaker at the March 17 edition of the [Colloquium d'Informatique de L'UPMC Sorbonne 
 Universités](https://www.lip6.fr/colloquium/?guest=Gardner). 
 
-These monthly Colloquia are organised by the [Laboratoire d’informatique de Paris 6 (LIP6)](https://www.lip6.fr/), a computer science research laboratory 
+Philippa gave a talk entitled "Understanding and Verifying JavaScript Programs", where she described JaVerT, a JavaScript Verification Toolchain 
+which provides the first logic-based symbolic analysis tool for JavaScript. The monthly Colloquia are organised 
+by the [Laboratoire d’informatique de Paris 6 (LIP6)](https://www.lip6.fr/), a computer science research laboratory 
 in the [Pierre et Marie Curie University](http://www.upmc.fr/en/university.html) in Paris, France. LIP6 has focused its research on the modeling 
 and the resolution of fundamental problems driven by applications, as well as to the implementation 
-and the validation through academic and industrial partnerships. Philippa gave a talk entitled Understanding and Verifying JavaScript Programs, 
-where she described JaVerT, a JavaScript Verification Toolchain which provides the first logic-based symbolic analysis tool for JavaScript.
+and the validation through academic and industrial partnerships.
 ![Colloqium Poster Philippa Gardner March 17](/images/posts/Gardner-2017-03-28.jpg)
\ No newline at end of file

_posts/2017-04-24-Dosualdo.md

@@ -9,4 +9,4 @@ at the University of Oxford under the supervision of Prof Luke Ong, winning the
 Emanuele joins us from the [Concurrency Theory Group at the University of Kaiserslautern]( http://concurrency.cs.uni-kl.de/), Germany
 where he worked with [Prof Roland Meyer]( http://concurrency.cs.uni-kl.de/group/meyer/home.html). His current work focuses 
 on models of concurrent behaviour to enable the construction of automatic analyses for concurrent systems.
-More details on his [webpage:](http://www.emanueledosualdo.com/research/)
+More details on his [webpage](http://www.emanueledosualdo.com/research/).

_posts/2017-04-28-fsen.md

@@ -2,7 +2,7 @@
 title: Keynote address at IPM FSEN Conference 2017, Iran
 ---
 Philippa Gardner was one of the keynote speakers at the [7th IPM International Conference on Fundamentals
-of Software Engineering]( http://fsen.ir/2017/Default.aspx) (FSEN 2017) held in Tehran, Iran
+of Software Engineering]( http://fsen.ir/2017/Default.aspx) (FSEN 2017) held in Tehran, Iran.
 
 Philippa’s talk, “Understanding and Verifying JavaScript Programs” was delivered
 by video link to an engaged audience composed of Iranian and international researchers,

_posts/2017-05-03-consistency.md

 ---
 title: Philippa Gardner, talk at the open Workshop on Consistency in Distributed Storage Systems, LIP6, Paris
 ---
-Philippa Gardner gave at talk on A Concurrent Specification of PoSIX at the open workshop [“Consistency in distributed storage.”](https://pages.lip6.fr/Marc.Shapiro/workshop-2017-05-03/)
-held at the Université Pierre et Marie Curie - LIP6, Paris, France on 3 May 2017.
+Philippa Gardner gave a talk on "A Concurrent Specification of PoSIX" at the open workshop "[Consistency in distributed storage](https://pages.lip6.fr/Marc.Shapiro/workshop-2017-05-03/)".
+organised by [Marc Shapiro](https://pages.lip6.fr/Marc.Shapiro/) [(UPMC-LIP6 and  Inria)](https://www.inria.fr/).
 
-The workshop, organised by [Marc Shapiro](https://pages.lip6.fr/Marc.Shapiro/) [(UPMC-LIP6 and  Inria)](https://www.inria.fr/) offers students 
+This year's workshop, held at the Université Pierre et Marie Curie - LIP6, Paris, France on 3 May 2017, offered students 
 and academics an opportunity to share insights on the principles and practice of distributed data replication systems, 
-based on solid distributed algorithm and engineering principles. This workshop is held under the aegis of the French ANR Project RainbowFS, 
+based on solid distributed algorithm and engineering principles. The workshop is held under the aegis of the French ANR Project RainbowFS, 
 which aims to deconstruct consistency and to develop principled tools for the design, verification, deployment and monitoring, 
 and to use them for developing a correct-by-construction and efficient geo-scale petabyte-sized storage system.
 
-Philippa’s abstract and slides are available from the [workshop page](https://pages.lip6.fr/Marc.Shapiro/workshop-2017-05-03/).
\ No newline at end of file
+Philippa’s abstract and slides are available on the [workshop page](https://pages.lip6.fr/Marc.Shapiro/workshop-2017-05-03/).

_posts/2017-05-08-aarhus.md

@@ -4,11 +4,14 @@ title: Visit to Aarhus University and Aarhus Concurrency Workshop
 
 Philippa Gardner, Azalea Raad, Andrea Cerone and Emanuele D'Osualdo will be attending the [Aarhus Concurrency Workshop on Concurrency Theory](http://conferences.au.dk/acw/) and related topics at the end of month.
 
-The workshop will take place at the Department of Computer Science at [Aarhus University](http://cs.au.dk/research/) on May 30 and 31 and 
-is the latest in a series previously held at University of Kent, Imperial College London, York, University of Oxford, 
-Trinity College Dublin, Cambridge University, Newcastle, and Queen Mary. 
-
 This year's workshop is organised by [Thomas Dinsdale-Young](http://cs.au.dk/~tyoung/), who was previously a PhD and PostDoc with Philippa.
 Andrea Cerone will give a talk on [Algebraic Laws for Weak Consistency](http://conferences.au.dk/acw/abstracts/). 
+The workshop will take place at the Department of Computer Science 
+at [Aarhus University](http://cs.au.dk/research/) on May 30 and 31 and 
+is the latest in a series previously held at [University of Kent](https://www.cs.kent.ac.uk/events/kcw/), 
+[Imperial College London](http://multicore.doc.ic.ac.uk/icw2015/), [The University of York](https://www-users.cs.york.ac.uk/~miked/ycw2014/), 
+[University of Oxford](http://www.cs.ox.ac.uk/people/hongseok.yang/ccw12/index.html), [Trinity College Dublin](https://www.scss.tcd.ie/Vasileios.Koutavas/dcw2011/),
+[Cambridge University](https://www-users.cs.york.ac.uk/~miked//ccw2010/index.html), Newcastle, 
+and [Queen Mary](https://web.archive.org/web/20100606005049/http://www.eecs.qmul.ac.uk/~ohearn/Workshops/Concurrency09/).
 
-Aarhus is the second largest city in Denmark and is one of the 2017 [European Capitals of Culture](http://www.aarhus2017.dk/en/).
\ No newline at end of file
+Aarhus is the second largest city in Denmark and is one of the 2017 [European Capitals of Culture](http://www.aarhus2017.dk/en/).

_posts/2017-05-09-Kloos.md

+---
+title: Johannes Kloos, visitor from MPI
+---
+[Johannes Kloos]( https://people.mpi-sws.org/~jkloos/), a fourth-year PhD student at the [Max Planck Institute for Software Systems](https://www.mpi-sws.org/) 
+visited the group this week. 
+
+Johannes gave a talk to the group about his current research, on Reasoning about event-based concurrency with Asynchronous Liquid Separation Types.
+
+The talk abstract: I will present work on a program logic and associated type system for reasoning about asynchronous programs manipulating shared 
+mutable state. The logic and type system guarantee the absence of races and the preservation of user-specified invariants using a combination of two ideas: 
+refinement types and concurrent separation logic. The logic track ownership of shared state across concurrently posted tasks and allow reasoning about 
+ownership transfer between tasks using permissions. The type system integrated the logic with refinement types to reason about the contents of the heap, 
+in presence of asynchronous tasks. I will first demonstrate the type system on examples from OCaml, and afterwards sketch some preliminary 
+work in applying it to JavaScript.
\ No newline at end of file

_posts/2017-05-15-S-REPLS.md

----
-title: 6th South of England Regional Programming Language Seminar, UCL
----
-
-The [6th edition of S-REPLS](http://srepls6.cs.ucl.ac.uk/), organised by our colleague [Ilya Sergey](http://www.cs.ucl.ac.uk/cs_people/I.Sergey.html/) 
-will take place on May 25, 2017, at University College London.
-
-S-REPLS is a regular and informal meeting for those based in the South of England 
-with a professional interest—whether it be academic or commercial—in the semantics and implementation of programming languages. 
-The seminar is free of charge and lunch will be provided. For details and to register, please see their [webpage](http://srepls6.cs.ucl.ac.uk/)
-
-The next S-REPLS meeting will take place at the University of Warwick, 
-in late 2017, and is organised by [Andrzej Murawski](http://www2.warwick.ac.uk/fac/sci/dcs/people/andrzej_murawski/) and David Purser. 
-
-Details of previous S-REPLS meetings can be found on [here](http://dominic-mulligan.co.uk/?page_id=195)
\ No newline at end of file

_posts/2017-05-17-Gian.md

 ---
-title: Goodbye to Gian Ntzik, moving to Amadeus
+title: Goodbye to Dr Gian Ntzik, moving to Amadeus
 ---
-Best wishes to Gian Ntzik, who will move to [Amadeus](http://www.amadeus.com/web/amadeus/en_GB-GB/Amadeus-Home/About-us/Our-company/1319477448520-Page-AMAD_DetailPpal)
-in May to work in systems development and research.
+Best wishes to Dr Gian Ntzik, who will move to [Amadeus](http://www.amadeus.com/web/amadeus/en_GB-GB/Amadeus-Home/About-us/Our-company/1319477448520-Page-AMAD_DetailPpal)
+at the end of May to work in systems development and research.
 
 Amadeus is one of the top ten providers of sofware in the world, especialising in sofware for the travel and tourism industry.  
-Amadeus employs over 14,000 people worldwide and is currently the largest provider of global distribution (GDS) systems in the world.
-
-
-
+Amadeus employs over 14,000 people worldwide and is currently the largest provider of global distribution (GDS) systems in the world.
\ No newline at end of file

_posts/2017-05-18-ecma.md

----
-title: Philippa Gardner, Ecma TC39 meeting, Google, NY
----
-Philippa Gardner will attend the next meeting of the [TC39 – ECMAScript Task group standards committee meeting](http://www.ecma-international.org/memento/TC39-RF-TG.htm)
-at Google, NY at the end of the month. 
-
-Philippa will give her talk: "Towards Trustworthy Verification of JavaScript" as part of the Visions for the future of ECMAScript / Emerging technologies agenda.
-TC39-Royalty Free Task Group scope is the standardization of the general purpose, cross platform, vendor-neutral programming language ECMAScript (JavaScript). 
-This includes the language syntax, semantics, and libraries and complementary technologies that support the language.
\ No newline at end of file

_posts/2017-05-25-Azalea.md

+---
+title: Congratulations to Azalea Raad, joining the Max Planck Institute for Software Systems, Germany
+---
+
+Many congratulations to Dr Azalea Raad, who has accepted a position as a Postdoctoral Fellow at the 
+[Max Planck Institute for Software Systems](https://www.mpi-sws.org/) in Kaiserslautern, Germany, starting in July.
+
+Azalea will work with [Viktor Vafeiadis](https://people.mpi-sws.org/~viktor/) and [Derek Dreyer](https://people.mpi-sws.org/~dreyer/) 
+on weak memory models for transactions, a new exciting area with much left to explore. Azalea's thesis and recent publications are now available 
+on [her website](http://www.soundandcomplete.org/publications.html).
\ No newline at end of file