diff --git a/.htaccess b/.htaccess
index 21f0b599aaa2ce0e133a14907d6817a083c6dd17..750ad4cdb0143ae5d0d6f571ef82e488b18466a5 100644
--- a/.htaccess
+++ b/.htaccess
@@ -5,16 +5,16 @@ RewriteEngine on
# Rewrite former site subdomain pages to new site pages
RewriteCond %{HTTP_HOST} =www-rw.doc.ic.ac.uk
-RewriteRule ^ http://psvg.doc.ic.ac.uk/research/javascript.html [R=301,L]
+RewriteRule ^ http://vtss.doc.ic.ac.uk/research/javascript.html [R=301,L]
RewriteCond %{HTTP_HOST} =www-lrr.doc.ic.ac.uk
-RewriteRule ^papers.html http://psvg.doc.ic.ac.uk/publications/ [R=301,L]
+RewriteRule ^papers.html http://vtss.doc.ic.ac.uk/publications/ [R=301,L]
RewriteCond %{HTTP_HOST} =www-lrr.doc.ic.ac.uk
-RewriteRule ^ca($|/) http://psvg.doc.ic.ac.uk/research/concurrency.html [R=301,L]
+RewriteRule ^ca($|/) http://vtss.doc.ic.ac.uk/research/concurrency.html [R=301,L]
# Bump any other subdomain request that gets here over to the main psvg site
-RewriteCond %{HTTP_HOST} !=psvg.doc.ic.ac.uk
-RewriteRule ^(.*)$ http://psvg.doc.ic.ac.uk/$1 [R=301,L]
+RewriteCond %{HTTP_HOST} !=vtss.doc.ic.ac.uk
+RewriteRule ^(.*)$ http://vtss.doc.ic.ac.uk/$1 [R=301,L]
ErrorDocument 403 /403.html
ErrorDocument 404 /404.html
diff --git a/README.md b/README.md
index ad555bf5b3c01f1ddef875f60fdfa6ba572d61ec..94b4f5f569e034c2962d7138efe9a0a8bb9094c3 100644
--- a/README.md
+++ b/README.md
@@ -3,14 +3,14 @@ layout: page
title: PSVG Group Website Readme
---
-This readme file is published in its fully rendered form [on the website](https://psvg.doc.ic.ac.uk/README.html).
+This readme file is published in its fully rendered form [on the website](https://vtss.doc.ic.ac.uk/README.html).
-The source code for [this site](https://psvg.doc.ic.ac.uk) is [hosted on the DoC GitLab server](https://gitlab.doc.ic.ac.uk/resource-reasoning/psvg.doc.ic.ac.uk),
+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.
**DO NOT EDIT THE SOURCE CODE IN `/vol/rr/www`, IT IS ALL REPLACED EACH TIME THE SITE IS REBUILT FROM VERSION CONTROL**
-[](https://gitlab.doc.ic.ac.uk/resource-reasoning/psvg.doc.ic.ac.uk/commits/master)
+[](https://gitlab.doc.ic.ac.uk/resource-reasoning/vtss.doc.ic.ac.uk/commits/master)
[](https://gemnasium.com/6ba7afbbfda9adcba06f007cc565a29a)
## Managing Content
diff --git a/_config.yml b/_config.yml
index 8021b9fd99dc1ce99a775318b9e4c65c211cae4a..a9a15bd7e7cc613e33f18bf01088046d0bebea8d 100644
--- a/_config.yml
+++ b/_config.yml
@@ -3,7 +3,7 @@ subtitle: <a href="http://www.doc.ic.ac.uk">Department of Computing</a>, <a href
copyright: Imperial College London
baseurl: ""
-url: "https://psvg.doc.ic.ac.uk"
+url: "https://vtss.doc.ic.ac.uk"
markdown: kramdown
diff --git a/_people/da-rocha-pinto.md b/_people/da-rocha-pinto.md
index 7e77ec63224e6439db4fd4ca0340a01bca87533b..97e081e06d35a81fff8b5dfa83327123b028050c 100644
--- a/_people/da-rocha-pinto.md
+++ b/_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://psvg.doc.ic.ac.uk/publications/daRochaPinto2017Reasoning.html) in January 2017.
+Pedro defended his PhD thesis, [Reasoning with Time and Data Abstractions](https://vtss.doc.ic.ac.uk/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.
diff --git a/_people/naudziuniene.md b/_people/naudziuniene.md
index 3d18585303021ec2fd91a3d5d4e5069915e117d1..dbe58459cf23eef1e27583608a3c13b7d1df9acf 100644
--- a/_people/naudziuniene.md
+++ b/_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://psvg.doc.ic.ac.uk/publications/Naudziuniene2018Infrastructure.html) in March 2018.
+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.
From 2017 Daviva has been working as a Research Scientist at Facebook as part of the engineering team led by Peter O’Hearn.
diff --git a/_people/ntzik.md b/_people/ntzik.md
index f504ec37924bb8250358900aec28b34b08dc5419..6ae520ac01102f3deb7c25118ce9c07a245ba006 100644
--- a/_people/ntzik.md
+++ b/_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://psvg.doc.ic.ac.uk/publications/Ntzik2017Reasoning.html)
+Gian defended his thesis [Reasoning about POSIX File Systems](https://vtss.doc.ic.ac.uk/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.
diff --git a/_people/raad.md b/_people/raad.md
index 3c60c0bc2a9699e60aceb5c9c19ae1f83f5ab1c9..d62df55c86a55b3f3750b8362c56192b32b799fd 100644
--- a/_people/raad.md
+++ b/_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://psvg.doc.ic.ac.uk/publications/Raad2017Abstraction.html) in February 2017.
+on [Abstraction, Refinement and Concurrent Reasoning](https://vtss.doc.ic.ac.uk/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/).
diff --git a/_posts/2016-10-03-papers.md b/_posts/2016-10-03-papers.md
index b24299da7ec9ecfdb35f3ec8a5ccb2a75a6f3a37..6f1f0a7a52b5480beb53cf048054801de5ac8f1a 100644
--- a/_posts/2016-10-03-papers.md
+++ b/_posts/2016-10-03-papers.md
@@ -3,6 +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).
+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://psvg.doc.ic.ac.uk/publications/).
+These and other group papers can be found on our [publications page](http://vtss.doc.ic.ac.uk/publications/).
diff --git a/_posts/2016-11-14-inferlab.md b/_posts/2016-11-14-inferlab.md
index 002e699b26acfcd7998ebf62119ea0f145e93fa1..01ca6fab6caa064a4f3469e0c8217f5ee3f12dfa 100644
--- a/_posts/2016-11-14-inferlab.md
+++ b/_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](https://vtss.doc.ic.ac.uk/teaching/separationlogic.html) 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](https://vtss.doc.ic.ac.uk/teaching/InferLab.html) page.
\ No newline at end of file
diff --git a/_posts/2016-12-15-Dolby.md b/_posts/2016-12-15-Dolby.md
index fa434990fb5ededf99fdf7d86199c43e8645ec0d..d75cd5615a817b1795c44e30195e432924062235 100644
--- a/_posts/2016-12-15-Dolby.md
+++ b/_posts/2016-12-15-Dolby.md
@@ -7,7 +7,7 @@ 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)
+in a [symbolic analysis for JavaScript](https://vtss.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
diff --git a/_posts/2017-01-13-Pedro_viva.md b/_posts/2017-01-13-Pedro_viva.md
index 5a9c99d6110298fd9d92f0c51e681a0281c3cbde..d1f2036da1337e89de8c3ec93df2d7e306574e15 100644
--- a/_posts/2017-01-13-Pedro_viva.md
+++ b/_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://psvg.doc.ic.ac.uk/publications/daRochaPinto2014TaDA.html) for verifying concurrent programs with much better support for abstraction.
+called [TaDA](https://vtss.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).
+Pedro's latest paper, accepted to ESOP 2017 is on [our publications page](https://vtss.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html).
diff --git a/_posts/2017-02-01-Gian_viva.md b/_posts/2017-02-01-Gian_viva.md
index d3df0e3435a7ca873e18d49459086477b2c1b22c..6fe6de06a929f715cf17c88c98872eb8ee9010fa 100644
--- a/_posts/2017-02-01-Gian_viva.md
+++ b/_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://vtss.doc.ic.ac.uk/people/ntzik.html).
diff --git a/_posts/2017-02-06-ESOP.md b/_posts/2017-02-06-ESOP.md
index a450a3ba06166fb50e3a04a1aa588b55fcd50cda..bb0589c4cbbf1186557c7f4fcc532142c21529a5 100644
--- a/_posts/2017-02-06-ESOP.md
+++ b/_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](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.
-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](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
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](https://vtss.doc.ic.ac.uk/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.
diff --git a/_posts/2017-06-16-Algebraic.md b/_posts/2017-06-16-Algebraic.md
index 5939f503b1cbe89be75345c814d641b76c82e82f..8a48f471ca6a435847739275879c97830fcb0fb0 100644
--- a/_posts/2017-06-16-Algebraic.md
+++ b/_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://psvg.doc.ic.ac.uk/publications/Cerone2017Algebraic.html) was written in collaboration
+The paper, entitled [Algebraic Laws for Weak Consistency](https://vtss.doc.ic.ac.uk/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.
diff --git a/_posts/2017-08-12-cade.md b/_posts/2017-08-12-cade.md
index a11b035e72a202e46ed7ee9f2010bab29e201cb6..857ad804090c8bb353304918c6b5034348f41493 100644
--- a/_posts/2017-08-12-cade.md
+++ b/_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://psvg.doc.ic.ac.uk/people/fragoso-santos.html), [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/)
+jointly written with [José Fragoso Santos](https://vtss.doc.ic.ac.uk/people/fragoso-santos.html), [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.
diff --git a/_posts/2017-09-26-popl.md b/_posts/2017-09-26-popl.md
index 126735da01ddd8b68447cf5a3992498ec6b18198..faf6005fdc8aea4fc4d60135b47d1fc1a04dcd84 100644
--- a/_posts/2017-09-26-popl.md
+++ b/_posts/2017-09-26-popl.md
@@ -1,7 +1,7 @@
---
title: Paper accepted at POPL 2018
---
-[José Fragoso Santos](https://psvg.doc.ic.ac.uk/people/fragoso-santos.html), [Philippa Gardner](https://www.doc.ic.ac.uk/~pg/),
+[José Fragoso Santos](https://vtss.doc.ic.ac.uk/people/fragoso-santos.html), [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/).
diff --git a/_posts/2017-10-02-gabriela.md b/_posts/2017-10-02-gabriela.md
index 9385d037b45e3760fed0ca3cccda245f503f8906..85d71c5bd78a17461098c01d0f824d3f48ddfd91 100644
--- a/_posts/2017-10-02-gabriela.md
+++ b/_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://psvg.doc.ic.ac.uk/people/sampaio.html), who has joined the group as a PhD student.
+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.
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),
diff --git a/_posts/2018-01-06-PhD_opportunity.md b/_posts/2018-01-06-PhD_opportunity.md
index 5b3dd8884236b569ea6e36bc8b6450d4aa04422e..1a3cf98fdb30f023660a849c74250c0ca377005f 100644
--- a/_posts/2018-01-06-PhD_opportunity.md
+++ b/_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://psvg.doc.ic.ac.uk/),
+to join the [Verified Trustworthy Software Specification Group](https://vtss.doc.ic.ac.uk/),
For more details, please see the note below from Philippa:
diff --git a/_posts/2018-01-12-popl.md b/_posts/2018-01-12-popl.md
index f8a05e06d6ccf05ec64c41d9419f205432b7d724..d278ce396875c4cdb7e4c0433c5deaea2e5db8c9 100644
--- a/_posts/2018-01-12-popl.md
+++ b/_posts/2018-01-12-popl.md
@@ -2,8 +2,8 @@
title: Paper presented at POPL18
---
-[José Fragoso Santos](https://psvg.doc.ic.ac.uk/people/fragoso-santos.html) presented his paper
-[JaVerT: JavaScript Verification using Separation Logic](https://psvg.doc.ic.ac.uk/publications/FragosoSantos2018JaVerT.html), jointly authored
+[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
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/).
diff --git a/_posts/2018-03-01-daiva-thesis.md b/_posts/2018-03-01-daiva-thesis.md
index 0c4eeeff8fe39d67fd7f95a6485cb400f105105f..bbeab1fea887c633f8a7081db67b36f67989f29d 100644
--- a/_posts/2018-03-01-daiva-thesis.md
+++ b/_posts/2018-03-01-daiva-thesis.md
@@ -4,7 +4,7 @@ title: Congratulations to Dr Daiva Naudžiūnienė
Many congratulations to [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/),
who very successfully defended her PhD thesis, [An Infrastructure for Tractable
-Verification of JavaScript Programs]( https://psvg.doc.ic.ac.uk/publications/Naudziuniene2018Infrastructure.html)
+Verification of JavaScript Programs]( https://vtss.doc.ic.ac.uk/publications/Naudziuniene2018Infrastructure.html)
on Monday 1st March.
Also many thanks to [Matthew Parkinson](https://www.microsoft.com/en-us/research/people/mattpark/),
diff --git a/_posts/2018-04-18-papers-accepted-april-18.md b/_posts/2018-04-18-papers-accepted-april-18.md
index 72369a8a7dbc166b980a05031b1bdf2311017cb5..add94751055f100ef3a9115ac64e9e430867767f 100644
--- a/_posts/2018-04-18-papers-accepted-april-18.md
+++ b/_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://psvg.doc.ic.ac.uk/people/da-rocha-pinto.html)
-and [Philippa Gardner](https://psvg.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](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).
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://psvg.doc.ic.ac.uk/people/ntzik.html),
-[Pedro da Rocha Pinto](https://psvg.doc.ic.ac.uk/people/da-rocha-pinto.html),
-[Julian Sutherland](https://psvg.doc.ic.ac.uk/people/sutherland.html)
-and [Philippa Gardner](https://psvg.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](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
[(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,
diff --git a/_posts/2018-07-16-seminar.md b/_posts/2018-07-16-seminar.md
index 53a3745747633d6e763524842885fdb90b2e64f3..74bf8a2d05004e7648abc13e3fec835f3799e6d7 100644
--- a/_posts/2018-07-16-seminar.md
+++ b/_posts/2018-07-16-seminar.md
@@ -15,7 +15,7 @@ to the environment as a result of interference by the intruder?
This project's goal is to develop a new algorithm to verify secrecy of cryptographic
protocols with unbounded sessions and nonces.
The novelty of the approach, based on a new decidability result
-by [D'Osualdo et al.(CSF17)](http://psvg.doc.ic.ac.uk/publications/DOsualdo2017Deciding.html),
+by [D'Osualdo et al.(CSF17)](http://vtss.doc.ic.ac.uk/publications/DOsualdo2017Deciding.html),
is in how the unboundedness caused by the use of unlimited nonces can be tamed
algorithmically. We will present a new verification algorithm for secrecy based
on symbolic representations of inductive invariants of protocols.
\ No newline at end of file
diff --git a/ci/.htaccess b/ci/.htaccess
index 9e0871d3d343afb94d35a6d66f90f836cd2aa309..68e89b660998de7b9e9b8f600e5941e547b6c84a 100644
--- a/ci/.htaccess
+++ b/ci/.htaccess
@@ -1,7 +1,7 @@
RewriteEngine On
-<If "%{HTTPS} == 'off' || %{HTTP_HOST} != 'psvg.doc.ic.ac.uk'">
- RewriteRule ^/vol/rr/www/(.*) https://psvg.doc.ic.ac.uk/$1 [R=301,L]
+<If "%{HTTPS} == 'off' || %{HTTP_HOST} != 'vtss.doc.ic.ac.uk'">
+ RewriteRule ^/vol/rr/www/(.*) https://vtss.doc.ic.ac.uk/$1 [R=301,L]
</If>
<Else>
AuthType KerberosV5
diff --git a/robots.txt b/robots.txt
index bfd45246a06e1b667114058d1486c37206cdaeb0..6fc2339724c50c5426afdc46a8ab3ba3b68b4ab5 100644
--- a/robots.txt
+++ b/robots.txt
@@ -1 +1 @@
-Sitemap: https://psvg.doc.ic.ac.uk/sitemap.xml
+Sitemap: https://vtss.doc.ic.ac.uk/sitemap.xml
diff --git a/teaching/InferLab.md b/teaching/InferLab.md
index 2f04ddedb768ac3e9a429e8743ff2e0f98a44aa3..852a32567fd914e48f6cee8a0e71ad905267a3e1 100644
--- a/teaching/InferLab.md
+++ b/teaching/InferLab.md
@@ -7,11 +7,11 @@ menu_order: 5
sub_menu_order: 2
---
-The [Separation Logic](https://psvg.doc.ic.ac.uk/teaching/separationlogic.html) course is a 4th-year MEng and MSc course
+The [Separation Logic](https://vtss.doc.ic.ac.uk/teaching/separationlogic.html) 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://psvg.doc.ic.ac.uk/people/sutherland.html).
+[Azalea Raad](http://www.soundandcomplete.org/) and [Julian Sutherland](https://vtss.doc.ic.ac.uk/people/sutherland.html).
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/),
diff --git a/teaching/separationlogic.md b/teaching/separationlogic.md
index 8c15eb673580cee58b321621d9724abffc5f011b..cff7f4dae6fa59ca99f70c2eb5b11d2b58f7cabe 100644
--- a/teaching/separationlogic.md
+++ b/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://psvg.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](https://vtss.doc.ic.ac.uk/teaching/InferLab.html) 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.