Tidy up various news posts for typos and punctuation

_posts/2016-07-26-advert.md

@@ -3,13 +3,13 @@ title: One new postdoc position at Imperial College
 ---
 We are looking to recruit one postdoctoral researcher in the Program Specification and Verification Group at Imperial College London, to work on reasoning about concurrent programs. The position is suitable for either a theoretician, who would work on the foundations of concurrent reasoning, or a theoretician/practitioner, who would work on the verification and testing of file systems.
 
-<b> \*\*\* Deadline: 18th September \*\*\* </b>
+<b> \*\*\* Applications now closed \*\*\* </b>
 
 This position will have an initial duration of 2.5 years, with a certain level of flexibility with respect to the start date and possible extensions. It will be funded as part of the £5.6M EPSRC Programme Grant ["REMS: Rigorous Engineering of Mainstream Systems"](https://www.cl.cam.ac.uk/~pes20/rems/index.html), at the University of Cambridge, University of Edinburgh, and Imperial College London
 
 The Department of Computing at Imperial provides a vibrant and stimulating research environment in the heart of London, with leading research groups working on programming languages, verification, and testing. The quality of the Department has been consistently awarded the highest research and teaching rating. In the latest Research Excellence Framework assessment of 2014, the Department was ranked third (first in the Research Intensity table published by the Times Higher). In addition, at the last national assessment of teaching quality, the Department was rated as "Excellent" and came 2nd in The Complete University Guide, The Guardian, The Times and The Sunday Times national league tables by subject.
 
-The Program Specification and Verification Group is led by Professor Philippa Gardner, and its current focus is on reasoning about JavaScript and concurrency. The advertised position will target concurrency in particular (see http://psvg.doc.ic.ac.uk/research/concurrency.html). The breadth of the REMS project allows for flexibility in the profile of the candidate, who would work either on the foundations of concurrency reasoning or on the verification and testing of file systems.
+The Program Specification and Verification Group is led by Professor Philippa Gardner, and its current focus is on reasoning about JavaScript and concurrency. The advertised position will target [concurrency](/research/concurrency.html) in particular. The breadth of the REMS project allows for flexibility in the profile of the candidate, who would work either on the foundations of concurrency reasoning or on the verification and testing of file systems.
 
 <b> \*\*\* Foundations of concurrency reasoning \*\*\* </b> Recently, various program logics based on concurrent separation logic have been developed, by ourselves and others, with the aim of providing more modular abstract reasoning about concurrent programs. Our work at Imperial has tackled a range of problems, including data abstraction (Concurrent Abstract Predicates), abstract atomicity (the TaDA logic), fault-tolerance and progress, applying our reasoning to concurrent B-trees, skip lists from java.util.concurrent, graph algorithms, and the POSIX file system. The advertised position is suitable for someone interested in such foundational work on concurrency reasoning and, in particular, its relationship with respect to linearisability.
 

_posts/2016-09-01-newmember.md

@@ -5,6 +5,6 @@ We are very happy to welcome Andrea Cerone to the group. Andrea has joined us fr
 
 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://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/).

_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 PSVG 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) 
 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

@@ -9,5 +9,6 @@ and to [Susan Eisenbach](http://www.imperial.ac.uk/people/s.eisenbach), who acte
 
 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](https://psvg.doc.ic.ac.uk/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](https://psvg.doc.ic.ac.uk/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](https://psvg.doc.ic.ac.uk/people/ntzik.html).

_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-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-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/)
+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/).
 
-
-
 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. 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 on 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

@@ -12,6 +12,6 @@ is the latest in a series previously held at [University of Kent](https://www.cs
 [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/).
+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-06-13-csf.md

@@ -4,7 +4,7 @@ title: Paper accepted at CSF'17
 Emanuele D'Osualdo has had a paper accepted at this year's [Computer Security Foundations Symposium (CSF)](http://csf2017.tecnico.ulisboa.pt/index.html).
 
 Emanuele's paper, in collaboration with [Luke Ong](http://www.cs.ox.ac.uk/luke.ong/), University of Oxford, UK and [Alwen Tiu](http://www.ntu.edu.sg/home/atiu/), 
-Nanyang Technological University, Singapore, is entitled ['Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes'](http://www.emanueledosualdo.com/research/papers/2017/csf-decidable-secrecy.html)
+Nanyang Technological University, Singapore, is entitled ['Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes'](http://www.emanueledosualdo.com/research/papers/2017/csf-decidable-secrecy.html).
 
 In the paper, the authors introduce a new class of security protocols with an unbounded number of sessions and unlimited fresh data 
 for which the problem of secrecy is decidable. The only constraint placed on the class is a notion of depth-boundedness. 
@@ -16,4 +16,4 @@ CSF'17 is an annual conference for researchers in computer security, to examine
 the formal models that provide a context for those theories, and techniques for verifying security. 
 Originally a workshop of the [IEEE Computer Society's Technical Committee on Security and Privacy](http://www.ieee-security.org/), 
 the meeting became a “symposium” in 2007, with a number of important papers and techniques having been presented first at CSF. 
-This year's papers are now available on the [CSF'17 conference's website](http://csf2017.tecnico.ulisboa.pt/accepted.html)
\ No newline at end of file
+This year's papers are now available on the [CSF'17 conference's website](http://csf2017.tecnico.ulisboa.pt/accepted.html).