ALL RELATIVE LINKS YESS

README.md

 ---
 layout: page
-title: PSVG Group Website Readme
+title: VTSS Group Website Readme
 ---
 
-This readme file is published in its fully rendered form [on the website](https://vtss.doc.ic.ac.uk/README.html).
+This readme file is published in its fully rendered form [on the website]({{site.baseurl}}{% link README.md %}).
 
 The source code for [this site](https://vtss.doc.ic.ac.uk) is [hosted on the DoC GitLab server](https://gitlab.doc.ic.ac.uk/resource-reasoning/vtss.doc.ic.ac.uk),
 you should have access to edit it if a member of the resource-reasoning group.

_people/da-rocha-pinto.md

@@ -9,5 +9,5 @@ alumnus: true
 ---
 Pedro was a PhD student and a Post Doc in the group, working on developing logics for verification of fine-grained concurrent programs. 
 
-Pedro defended his PhD thesis, [Reasoning with Time and Data Abstractions](https://vtss.doc.ic.ac.uk/publications/daRochaPinto2017Reasoning.html) in January 2017.
+Pedro defended his PhD thesis, [Reasoning with Time and Data Abstractions]({{site.baseurl}}{% link publications/daRochaPinto2017Reasoning.html %}) in January 2017.
 He is currently working for [Collage.com, Inc.](https://www.collage.com/) a Michigan-based photo products e-commerce company.

_people/naudziuniene.md

@@ -6,7 +6,7 @@ webpage: http://www.doc.ic.ac.uk/~dn911/
 email: d.naudziuniene11@imperial.ac.uk
 alumnus: true
 ---
-Daiva defended her Ph.D. on [An Infrastructure for Tractable Verification of JavaScript Programs](https://vtss.doc.ic.ac.uk/publications/Naudziuniene2018Infrastructure.html) in March 2018.
+Daiva defended her Ph.D. on [An Infrastructure for Tractable Verification of JavaScript Programs]({{site.baseurl}}{% link publications/Naudziuniene2018Infrastructure.html %}) in March 2018.   
 
 From 2017 Daviva has been working as a Research Scientist at Facebook as part of the engineering team led by Peter O’Hearn.
 

_people/ntzik.md

@@ -11,7 +11,7 @@ alumnus: true
 Gian Ntzik, Phd student and Post Doc with the group. 
 
 
-Gian defended his thesis [Reasoning about POSIX File Systems](https://vtss.doc.ic.ac.uk/publications/Ntzik2017Reasoning.html) 
+Gian defended his thesis [Reasoning about POSIX File Systems]({{site.baseurl}}{% link publications/Ntzik2017Reasoning.html %}) 
 in February 2017 and is currently working 
 for [Amadeus](http://www.amadeus.com/web/amadeus/en_GB-GB/Amadeus-Home/About-us/Our-company/1319477448520-Page-AMAD_DetailPpal) 
 in systems development and research.

_people/raad.md

@@ -8,7 +8,7 @@ alumnus: true
 ---
 
 Azalea Raad was a PhD student with the group, defending her thesis 
-on [Abstraction, Refinement and Concurrent Reasoning](https://vtss.doc.ic.ac.uk/publications/Raad2017Abstraction.html) in February 2017.
+on [Abstraction, Refinement and Concurrent Reasoning]({{site.baseurl}}{% link publications/Raad2017Abstraction.html %}) in February 2017.
 She is now a postdoctoral researcher at the [Max Planck Institute for Software Systems (Kaiserslautern)](https://www.mpi-sws.org/), 
 working with [Derek Dreyer](https://people.mpi-sws.org/~dreyer/) and [Viktor Vafeiadis](https://people.mpi-sws.org/~viktor/)
 and a member of the [ERC RustBelt project](http://plv.mpi-sws.org/rustbelt/).

_posts/2016-11-14-inferlab.md

@@ -2,7 +2,7 @@
 title: Infer Lab at Imperial
 ---
 
-The [Separation Logic](https://vtss.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://vtss.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-12-15-Dolby.md

@@ -3,11 +3,11 @@ 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.
+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://vtss.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 

_posts/2017-01-13-Pedro_viva.md

@@ -10,6 +10,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://vtss.doc.ic.ac.uk/publications/daRochaPinto2014TaDA.html) for verifying concurrent programs with much better support for abstraction.
+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](https://vtss.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html).
+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://vtss.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://vtss.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://vtss.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://vtss.doc.ic.ac.uk/people/xiong.html), [Pedro Da Rocha Pinto](https://vtss.doc.ic.ac.uk/people/da-rocha-pinto.html), 
-[Gian Ntzik](https://vtss.doc.ic.ac.uk/people/ntzik.html) and [Philippa Gardner](https://vtss.doc.ic.ac.uk/people/gardner.html),
-[Abstract Specifications for Concurrent Maps](https://vtss.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://vtss.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-06-16-Algebraic.md

@@ -4,7 +4,7 @@ title: Paper accepted at Concur 2017
 Andrea Cerone has had a paper accepted at this year’s [International Conference on Concurrency Theory, (Concur 2017)](https://www.concur2017.tu-berlin.de/) 
 which will be held in Berlin, Germany in September.
 
-The paper, entitled [Algebraic Laws for Weak Consistency](https://vtss.doc.ic.ac.uk/publications/Cerone2017Algebraic.html) was written in collaboration 
+The paper, entitled [Algebraic Laws for Weak Consistency]({{site.baseurl}}{% link publications/Cerone2017Algebraic.html %}) was written in collaboration 
 with [Alexey Gotsman]( http://software.imdea.org/~gotsman), IMDEA Software Institute, Madrid and [Hongseok Yang](http://www.cs.ox.ac.uk/people/hongseok.yang/Public/Home.html), University of Oxford, UK.
 
 The purpose of the CONCUR conferences is to bring together researchers, developers, and students in order to advance the theory of concurrency, and promote its applications. The topics covered are Theory, Formal Modelling, Verification, Performance Evaluation and Engineering of concurrent, timed, and other systems.

_posts/2017-08-12-cade.md

@@ -5,7 +5,7 @@ title: Invited paper at the 26th International Conference on Automated Reasoning
 Philippa Gardner was one of the invited speakers at the this year’s [CADE conference](http://www.cade-26.info/), held in Gothenburg, Sweden, on 6-11 August 2017. 
 
 Philippa presented an invited paper, [‘Towards Logic-based Verification of JavaScript Programs’](https://link.springer.com/chapter/10.1007/978-3-319-63046-5_2), 
-jointly written with [José Fragoso Santos](https://vtss.doc.ic.ac.uk/people/fragoso-santos.html), [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/) 
+jointly written with [José Fragoso Santos]({{site.baseurl}}{% link _people/fragoso-santos.md %}), [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/) 
 and [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/) 
 
 This position paper proposes a possible pathway to achieve scalable symbolic verification of JavaScript based on separation logic. 

_posts/2017-09-26-popl.md

 ---
 title: Paper accepted at POPL 2018
 ---
-[José Fragoso Santos](https://vtss.doc.ic.ac.uk/people/fragoso-santos.html), [Philippa Gardner](https://www.doc.ic.ac.uk/~pg/), 
+[José Fragoso Santos]({{site.baseurl}}{% link _people/fragoso-santos.md %}), [Philippa Gardner](https://www.doc.ic.ac.uk/~pg/), 
 [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/), [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/) 
 and [Thomas Wood](https://www.doc.ic.ac.uk/~tw1509/), have had a paper accepted at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages 
 [(POPL 2018)](https://popl18.sigplan.org/).

_posts/2017-10-02-gabriela.md

@@ -4,7 +4,7 @@ title: Welcome to Gabriela Sampaio, new PhD student with the group
 
 ---
 
-We are really happy to welcome [Gabriela Sampaio](https://vtss.doc.ic.ac.uk/people/sampaio.html), who has joined the group as a PhD student. 
+We are really happy to welcome [Gabriela Sampaio]({{site.baseurl}}{% link _people/sampaio.md %}), who has joined the group as a PhD student. 
 
 Gabriela completed her BSc at the Federal University of Pernambuco (UFPE, Brazil)
 and as an undergraduate, she spent a year at the University of Kent, working on [Wrangler](https://www.cs.kent.ac.uk/projects/wrangler/Wrangler/Home.html), 

_posts/2018-01-06-PhD_opportunity.md

@@ -3,7 +3,7 @@ title: PhD position, start date in October 2018
 ---
 
 Philippa Gardner is currently looking for a PhD student, start date in October 2018, 
-to join the [Verified Trustworthy Software Specification Group](https://vtss.doc.ic.ac.uk/), 
+to join the [Verified Trustworthy Software Specification Group]({{site.baseurl}}), 
  
 
 For more details, please see the note below from Philippa:

_posts/2018-01-12-popl.md

@@ -2,8 +2,8 @@
 title: Paper presented at POPL18
 ---
 
-[José Fragoso Santos](https://vtss.doc.ic.ac.uk/people/fragoso-santos.html) presented his paper 
-[JaVerT: JavaScript Verification using Separation Logic](https://vtss.doc.ic.ac.uk/publications/FragosoSantos2018JaVerT.html), jointly authored 
+[José Fragoso Santos]({{site.baseurl}}{% link _people/fragoso-santos.md %}) presented his paper 
+[JaVerT: JavaScript Verification using Separation Logic]({{site.baseurl}}{% link publications/FragosoSantos2018JaVerT.html %}), jointly authored 
 with [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/), [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/),
 [Thomas Wood](https://www.doc.ic.ac.uk/~tw1509/) and [Philippa Gardner](https://www.doc.ic.ac.uk/~pg/), at this year’s ACM SIGPLAN Symposium on Principles 
 of Programming Languages [(POPL 2018)](https://popl18.sigplan.org/).

_posts/2018-04-18-papers-accepted-april-18.md

@@ -7,8 +7,8 @@ publised. A second paper, also collaborative work with current and former resear
 has also just been accepted to ECOOP 18.
 
 The first paper, [A perspective on specifying and verifying concurrent modules](https://www.sciencedirect.com/science/article/pii/S2352220817300871)
-by [Thomas Dinsdale-Young](https://cs.au.dk/~tyoung/), [Pedro da Rocha Pinto](https://vtss.doc.ic.ac.uk/people/da-rocha-pinto.html) 
-and [Philippa Gardner](https://vtss.doc.ic.ac.uk/people/gardner.html) has been published in the [Journal of Logical and Algebraic Methods in Programming](https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming).
+by [Thomas Dinsdale-Young](https://cs.au.dk/~tyoung/), [Pedro da Rocha Pinto]({{site.baseurl}}{% link _people/da-rocha-pinto.md %}) 
+and [Philippa Gardner]({{site.baseurl}}{% link _people/gardner.md %}) has been published in the [Journal of Logical and Algebraic Methods in Programming](https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming).
 
 In the paper, the authors survey a range of techniques for specifying concurrent modules, 
 using the example of a counter module to illustrate the benefits and limitations of each.
@@ -18,10 +18,10 @@ these concepts can be combined to achieve two powerful approaches for specifying
 concurrent modules and verifying implementations and clients, which remove the 
 limitations highlighted by the counter example.
 
-The second paper, co-authored by [Gian Ntzik](https://vtss.doc.ic.ac.uk/people/ntzik.html), 
-[Pedro da Rocha Pinto](https://vtss.doc.ic.ac.uk/people/da-rocha-pinto.html), 
-[Julian Sutherland](https://vtss.doc.ic.ac.uk/people/sutherland.html)
-and [Philippa Gardner](https://vtss.doc.ic.ac.uk/people/gardner.html) has just been accepted to the 32nd European Conference on Object-Oriented Programming 
+The second paper, co-authored by [Gian Ntzik]({{site.baseurl}}{% link _people/ntzik.md %}), 
+[Pedro da Rocha Pinto]({{site.baseurl}}{% link _people/da-rocha-pinto.md %}), 
+[Julian Sutherland]({{site.baseurl}}{% link _people/sutherland.md %})
+and [Philippa Gardner]({{site.baseurl}}{% link _people/gardner.md %}) has just been accepted to the 32nd European Conference on Object-Oriented Programming 
 [(ECOOP 2018)](https://conf.researchr.org/home/ecoop-2018), which will be held in Amsterdam in July. 
 
 In the paper, entitled A Concurrent Specification of POSIX File Systems, 

teaching/InferLab.md

@@ -7,11 +7,11 @@ menu_order: 5
 sub_menu_order: 2
 ---
 
-The [Separation Logic](https://vtss.doc.ic.ac.uk/teaching/separationlogic.html) course is a 4th-year MEng and MSc course 
+The [Separation Logic]({{site.baseurl}}{% link teaching/separationlogic.md %}) course is a 4th-year MEng and MSc course 
 on local reasoning about programs that manipulate the heap at the [Department of Computing](http://www.imperial.ac.uk/computing),
 [Imperial College London](http://www.imperial.ac.uk). The course is led by [Philippa Gardner](/people/gardner.html), with support 
 from [Jose Fragoso](https://www.doc.ic.ac.uk/~jfaustin/), [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/), 
-[Azalea Raad](http://www.soundandcomplete.org/) and [Julian Sutherland](https://vtss.doc.ic.ac.uk/people/sutherland.html).
+[Azalea Raad](http://www.soundandcomplete.org/) and [Julian Sutherland]({{site.baseurl}}{% link _people/sutherland.md %}).
 
 As part of the course, [Peter O’Hearn](http://www.pl-enthusiast.net/2015/09/15/facebooks-peter-ohearn-on-programming-languages/) 
 and [Jules Villard](https://www.doc.ic.ac.uk/~jvillar1/) from Facebook came to Imperial College to talk about [Infer](http://fbinfer.com/), 

teaching/separationlogic.md

@@ -31,7 +31,7 @@ You will learn how to write program specifications and prove properties of progr
 You will learn about Smallfoot, a semi-automatic verification tool based on symbolic execution, and [Infer](http://fbinfer.com/), an automatic tool based on bi-abduction. 
 This work constitutes a breakthrough, in that it is now possible prove properties about millions of lines of code, thus making the reasoning viable for industry.
 
-    As part of the course, Facebook with Imperial ran a lab on Infer. See our [Infer lab 2016 page](https://vtss.doc.ic.ac.uk/teaching/InferLab.html) for details
+    As part of the course, Facebook with Imperial ran a lab on Infer. See our [Infer lab 2016 page]({{site.baseurl}}{% link teaching/InferLab.md %}) for details
 
 * The last week will provide an introduction to concurrent separation logics. With Brookes, O'Hearn won the Godel prize for this work in 2016.