.deploy.sh

+#!/bin/sh
+# Use rsync to transfer files to a server via ssh, ensuring that the files are transferred with the correct permissions,
+# user group. The command will also remove old files from the remote directory.
+# To transfer files to the default location, you will need to be a member of the `rr` DoC usergroup.
+#
+# Example usage:
+# DOC_DEPLOY_USER=me ./.deploy.sh
+
+set -x
+USER=${DOC_DEPLOY_USER:+${DOC_DEPLOY_USER}@}
+SERVER=${DOC_DEPLOY_SERVER:-shell1.doc.ic.ac.uk}
+PTH=${DOC_DEPLOY_PATH:-/vol/rr/www}
+exec rsync -e "ssh -o StrictHostKeyChecking=no" --chmod=Dg+s,ug+rwX,o+rX --chown=:rr -igrp --delete _site/ "${USER}${SERVER}:${PTH}"
+

.gitlab-ci.yml

@@ -3,74 +3,88 @@ stages:
   - build
   - deploy
 
-update_publications:
-  stage: update
-  script:
-    - git checkout -B ${CI_BUILD_REF_NAME}
-    - git submodule update --init --remote
-    - git add publications
-    - git commit -m "[AUTO] Updating publications submodule" || exit 0
-    - git remote rm rw || true
-    - git remote add rw git@gitlab.doc.ic.ac.uk:${CI_PROJECT_PATH}.git
-    - eval `ssh-agent`
-    - echo "$PUSH_KEY" | ssh-add -
-    - git push rw ${CI_BUILD_REF_NAME}
-  variables:
-    GIT_AUTHOR_NAME: Resource Reasoning Group Backup Bot
-    GIT_COMMITTER_NAME: Resource Reasoning Group Backup Bot
-    GIT_AUTHOR_EMAIL: rr-gitlab-bot@example.com
-    EMAIL: rr-gitlab-bot@example.com
-  image: ignoredambience/github-gitlab-sync
-  tags:
-    - docker
-  only:
-    - triggers
+image: "ruby:2.6-buster"
+variables:
+  NOKOGIRI_USE_SYSTEM_LIBRARIES: "true"
 
 build:
   stage: build
-  image: "ruby:2.4"
+  artifacts:
+    paths:
+      - _site/
+    expire_in: 1 day
+  cache:
+    paths:
+      - vendor/bundle/
+  except:
+    - triggers
   tags:
     - docker
+    - vtss_site
   before_script:
     - bundle install --deployment --without=development --with=test
     - bundle exec rake init
   script:
     - bundle exec rake -s --suppress-backtrace . test
-  artifacts:
-    paths:
-      - _site/
-    expire_in: 1 day
-  except:
-    - triggers
 
 deadlinks:
   stage: deploy
-  image: "ruby:2.4"
+  allow_failure: true
+  cache:
+    paths:
+      - vendor/bundle/
+  except:
+    - triggers
   tags:
     - docker
+    - vtss_site
   before_script:
     - bundle install --deployment --without=development --with=test
   script:
     - bundle exec rake -s --suppress-backtrace . testlinks
-  allow_failure: true
-  except:
-    - triggers
 
 deploy:
   stage: deploy
   environment: production
-  script:
-    - "umask 0002 && rsync --chmod=Dg+s,ug+rwX,o+rX --chown=:rr -igrp --delete _site/ /vol/rr/www"
+  image: resourcereasoning/website-deploy
   tags:
-    - auth-rr
+    - docker
+    - vtss_site
   only:
     - master
   except:
     - triggers
+  # DOC_DEPLOY_USER and DOC_DEPLOY_KEY should be defined as secret variables in the GitLab CI Settings panel
+  before_script:
+    - eval `ssh-agent`
+    - echo "$DOC_DEPLOY_KEY" | ssh-add -
+  script:
+    - ./.deploy.sh
 
-variables:
-  NOKOGIRI_USE_SYSTEM_LIBRARIES: "true"
-
-cache:
-  paths:
-    - vendor/bundle/
+# Special target triggered when publications repository is updated:
+update_publications:
+  stage: update
+  variables:
+    GIT_AUTHOR_NAME: Resource Reasoning Group Backup Bot
+    GIT_COMMITTER_NAME: Resource Reasoning Group Backup Bot
+    GIT_AUTHOR_EMAIL: rr-gitlab-bot@example.com
+    EMAIL: rr-gitlab-bot@example.com
+    # PUSH_KEY should be defined as a secret variable in the GitLab UI
+    SSH_KEY: $PUSH_KEY
+  image: ignoredambience/github-gitlab-sync
+  tags:
+    - docker
+    - vtss_site
+  only:
+    - triggers
+  before_script:
+    - eval `ssh-agent`
+    - echo "$SSH_KEY" | ssh-add -
+  script:
+    - git checkout -B ${CI_COMMIT_REF_NAME}
+    - git submodule update --init --remote
+    - git add publications
+    - git commit -m "[AUTO] Updating publications submodule" || exit 0
+    - git remote rm rw || true
+    - git remote add rw git@gitlab.doc.ic.ac.uk:${CI_PROJECT_PATH}.git
+    - git push rw ${CI_COMMIT_REF_NAME}

.gitmodules

 [submodule "publications"]
 	path = publications
-	url = https://gitlab.doc.ic.ac.uk/resource-reasoning/publications.git
+	url = https://gitlab.doc.ic.ac.uk/verified-software/publications.git
 	branch = master

.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

Dockerfile

+FROM ruby:2.6
+
+# throw errors if Gemfile has been modified since Gemfile.lock
+RUN bundle config --global frozen 1
+RUN gem install bundler:1.16.6
+
+WORKDIR /usr/src/app
+
+COPY Gemfile Gemfile.lock ./
+RUN bundle install
+
+COPY . .
+
+RUN bundle exec rake init
+
+EXPOSE 4000
+
+CMD ["bundle", "exec", "jekyll", "serve", "--host", "0.0.0.0"]
\ No newline at end of file

Gemfile

 source 'https://rubygems.org'
 
+Encoding.default_external = Encoding::UTF_8
+
 gem 'rake'
 group :build do
   gem 'jekyll'

Gemfile.lock

 GEM
   remote: https://rubygems.org/
   specs:
-    activesupport (5.1.4)
+    activesupport (5.2.1)
       concurrent-ruby (~> 1.0, >= 1.0.2)
-      i18n (~> 0.7)
+      i18n (>= 0.7, < 2)
       minitest (~> 5.1)
       tzinfo (~> 1.1)
     addressable (2.5.2)
       public_suffix (>= 2.0.2, < 4.0)
-    bibtex-ruby (4.4.4)
+    bibtex-ruby (4.4.7)
       latex-decode (~> 0.0)
-    citeproc (1.0.5)
-      namae (~> 0.8)
-    citeproc-ruby (1.1.7)
-      citeproc (>= 1.0.4, < 2.0)
-      csl (~> 1.4)
+    citeproc (1.0.9)
+      namae (~> 1.0)
+    citeproc-ruby (1.1.10)
+      citeproc (~> 1.0, >= 1.0.9)
+      csl (~> 1.5)
     colorator (1.1.0)
     colorize (0.8.1)
-    concurrent-ruby (1.0.5)
-    csl (1.4.5)
-      namae (~> 0.7)
-    csl-styles (1.0.1.8)
+    concurrent-ruby (1.1.3)
+    csl (1.5.0)
+      namae (~> 1.0)
+    csl-styles (1.0.1.9)
       csl (~> 1.0)
-    ethon (0.10.1)
+    em-websocket (0.5.1)
+      eventmachine (>= 0.12.9)
+      http_parser.rb (~> 0.6.0)
+    ethon (0.11.0)
       ffi (>= 1.3.0)
-    ffi (1.9.18)
+    eventmachine (1.2.7)
+    ffi (1.9.25)
     forwardable-extended (2.6.0)
-    html-proofer (3.7.3)
+    html-proofer (3.9.2)
       activesupport (>= 4.2, < 6.0)
       addressable (~> 2.3)
       colorize (~> 0.8)
       mercenary (~> 0.3.2)
-      nokogiri (~> 1.7)
+      nokogiri (~> 1.8.1)
       parallel (~> 1.3)
-      typhoeus (~> 0.7)
+      typhoeus (~> 1.3)
       yell (~> 2.0)
-    i18n (0.8.6)
-    jekyll (3.6.0)
+    http_parser.rb (0.6.0)
+    i18n (0.9.5)
+      concurrent-ruby (~> 1.0)
+    jekyll (3.8.5)
       addressable (~> 2.4)
       colorator (~> 1.0)
+      em-websocket (~> 0.5)
+      i18n (~> 0.7)
       jekyll-sass-converter (~> 1.0)
-      jekyll-watch (~> 1.1)
+      jekyll-watch (~> 2.0)
       kramdown (~> 1.14)
       liquid (~> 4.0)
       mercenary (~> 0.3.3)
       pathutil (~> 0.9)
-      rouge (>= 1.7, < 3)
+      rouge (>= 1.7, < 4)
       safe_yaml (~> 1.0)
-    jekyll-feed (0.9.2)
+    jekyll-feed (0.11.0)
       jekyll (~> 3.3)
-    jekyll-redirect-from (0.12.1)
+    jekyll-redirect-from (0.14.0)
       jekyll (~> 3.3)
-    jekyll-sass-converter (1.5.0)
+    jekyll-sass-converter (1.5.2)
       sass (~> 3.4)
-    jekyll-scholar (5.10.2)
+    jekyll-scholar (5.14.0)
       bibtex-ruby (~> 4.0, >= 4.0.13)
       citeproc-ruby (~> 1.0)
       csl-styles (~> 1.0)
       jekyll (~> 3.0)
-    jekyll-sitemap (1.1.1)
+    jekyll-sitemap (1.2.0)
       jekyll (~> 3.3)
-    jekyll-watch (1.5.0)
-      listen (~> 3.0, < 3.1)
-    kramdown (1.15.0)
-    latex-decode (0.2.2)
-      unicode (~> 0.4)
-    liquid (4.0.0)
-    listen (3.0.8)
+    jekyll-watch (2.1.2)
+      listen (~> 3.0)
+    kramdown (1.17.0)
+    latex-decode (0.3.1)
+    liquid (4.0.1)
+    listen (3.1.5)
       rb-fsevent (~> 0.9, >= 0.9.4)
       rb-inotify (~> 0.9, >= 0.9.7)
+      ruby_dep (~> 1.2)
     mercenary (0.3.6)
     mini_portile2 (2.3.0)
-    minitest (5.10.3)
-    namae (0.11.3)
-    nokogiri (1.8.1)
+    minitest (5.11.3)
+    namae (1.0.1)
+    nokogiri (1.8.5)
       mini_portile2 (~> 2.3.0)
-    parallel (1.12.0)
-    pathutil (0.16.0)
+    parallel (1.12.1)
+    pathutil (0.16.2)
       forwardable-extended (~> 2.6)
-    public_suffix (3.0.0)
-    rake (12.1.0)
-    rb-fsevent (0.10.2)
+    public_suffix (3.0.3)
+    rake (12.3.1)
+    rb-fsevent (0.10.3)
     rb-inotify (0.9.10)
       ffi (>= 0.5.0, < 2)
-    rouge (2.2.1)
+    rouge (3.3.0)
+    ruby_dep (1.5.0)
     safe_yaml (1.0.4)
-    sass (3.5.2)
+    sass (3.7.2)
       sass-listen (~> 4.0.0)
     sass-listen (4.0.0)
       rb-fsevent (~> 0.9, >= 0.9.4)
       rb-inotify (~> 0.9, >= 0.9.7)
     thread_safe (0.3.6)
-    typhoeus (0.8.0)
-      ethon (>= 0.8.0)
-    tzinfo (1.2.3)
+    typhoeus (1.3.1)
+      ethon (>= 0.9.0)
+    tzinfo (1.2.5)
       thread_safe (~> 0.1)
-    unicode (0.4.4.4)
     yell (2.0.7)
 
 PLATFORMS
@@ -111,4 +119,4 @@ DEPENDENCIES
   rake
 
 BUNDLED WITH
-   1.15.4
+   1.16.6

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://psvg.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://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**
 
-[![Build Status](https://gitlab.doc.ic.ac.uk/resource-reasoning/psvg.doc.ic.ac.uk/badges/master/build.svg)](https://gitlab.doc.ic.ac.uk/resource-reasoning/psvg.doc.ic.ac.uk/commits/master)
+[![Build Status](https://gitlab.doc.ic.ac.uk/resource-reasoning/vtss.doc.ic.ac.uk/badges/master/build.svg)](https://gitlab.doc.ic.ac.uk/resource-reasoning/vtss.doc.ic.ac.uk/commits/master)
 [![Dependency Status](https://gemnasium.com/bd81b2aa11ff43417700f75dbd194221.svg)](https://gemnasium.com/6ba7afbbfda9adcba06f007cc565a29a)
 
 ## Managing Content
@@ -93,7 +93,19 @@ are consistent.
 An additional check that external links are still live is also run, but this test is permitted to fail without blocking
 the deployment.
 
-The site is deployed to `/vol/rr/www` automatically on successful build.
+The site should be deployed automatically by GitLab CI. To deploy the site manually from your own machine, run the `.deploy.sh` script. This will use `rsync` to synchronise the contents of the `_site` directory with the webserver via SSH. Default deployment parameters:
+* DOC_DEPLOY_USER: the default username used by SSH to connect, usually the username on your local machine
+* DOC_DEPLOY_SERVER: `shell1.doc.ic.ac.uk`
+* DOC_DEPLOY_PATH: `/vol/rr/www`
+To override these parameters, set shell variables, eg: `DOC_DEPLOY_USER=me ./.deploy.sh`
+
+The site is deployed to `/vol/rr/www` automatically on successful build using the `.deploy.sh` script.
+The contents of the `DOC_DEPLOY_KEY` CI environment variable are used
+as the private key used to authenticate with the server. This key is currently configured to give locked-down rsync access to the
+`/vol/rr/www` using `pg`'s user account. For further details for how this is achieved, [see this
+howto](https://www.guyrutenberg.com/2014/01/14/restricting-ssh-access-to-rsync/). Note: when deploying to a locked-down
+rsync account, the DOC_DEPLOY_PATH should be set to a path relative to the lockdown path -- use `.` if in doubt. You
+won't need to set this if you're deploying from your own user account.
 
 Locally Building and Testing
 ----------------------------

Rakefile

@@ -35,3 +35,8 @@ desc "Build the site, rebuild when files are edited, and serve via a local http
 task :serve do
   sh "bundle exec jekyll serve"
 end
+
+desc "Deploy the website to the webserver"
+task :deploy do
+  sh ".deploy.sh"
+end

_config.yml

-title: Verified Trustworthy Software Specification Group
+title: Verified Software
 subtitle: <a href="http://www.doc.ic.ac.uk">Department of Computing</a>, <a href="http://www.imperial.ac.uk/">Imperial College London</a>
 copyright: Imperial College London
 
 baseurl: ""
-url: "https://psvg.doc.ic.ac.uk"
+url: "https://vtss.doc.ic.ac.uk"
 
 markdown: kramdown
 
+encoding: utf-8
+timezone: Europe/London
+
 include:
   - .htaccess
 exclude:

_data/external_assets.yml

@@ -26,8 +26,8 @@ fontawesome:
     integrity: "sha384-XdYbMnZ/QjLh6iI4ogqCTaIjrFk87ip+ekIjefZch0Y+PvJ8CDYtEs1ipDmPorQ+"
 
 mathjax:
-  uri: "http://cdn.mathjax.org/mathjax/"
-  version: "latest"
+  uri: "https://cdnjs.cloudflare.com/ajax/libs/mathjax/"
+  version: "2.7.5"
   js:
     path: "/MathJax.js?config=TeX-AMS-MML_HTMLorMML"
     async: true

_includes/alumni.html

@@ -6,7 +6,7 @@
   {% assign id = group.name | replace:' ','-' %}
   <div class="panel-heading">
     <h6 class="panel-title">
-      <a data-toggle="collapse" href="#{{id}}" style="color:black">{{position}} ↯</a>
+      <a data-toggle="collapse" href="#{{id}}" style="color:black">{{position}}s ↯</a>
     </h6>
   </div>
 

_includes/footer.html

 <footer class="site-footer">
-  <p>&copy; {{ site.time | date: "%Y" }} {{ site.copyright }}</p>
+  <p>&copy; {{ site.time | date: "%Y" }} {{ site.copyright }}<br />
+  <a href="https://www.imperial.ac.uk/about-the-site/privacy/">Privacy Notice</a> - <a href="{{ '/accessibility/' | relative_url }}">Accessibility</a></p>
 </footer>

_layouts/home.html

@@ -6,7 +6,7 @@ layout: default
     {{ content }}
   </div>
   {% assign research_pages = site.pages | where_exp: 'page', 'page.url contains "/research/"'%}
-  {% for item in research_pages reversed %}
+  {% for item in research_pages %}
   <a class="btn btn-primary btn-lg" href="{{ item.url }}">{{ item.title }}</a>
   {% endfor %}
 </div>

_layouts/person.html

@@ -13,7 +13,8 @@ menu: false
   </header>
 
 {% comment %} Test that we have main content to show {% endcomment %}
-{% capture bibliography %}{% bibliography -q @*[author ~= {{ page.lastname }}] %}{% endcapture %}
+{% if page.search_lastname %}{% assign search_lastname = page.search_lastname %}{% else %}{% assign search_lastname = page.lastname %}{% endif %}
+{% capture bibliography %}{% bibliography -q @*[author ~= {{ search_lastname }}] %}{% endcapture %}
 {% assign test_bib = bibliography | strip_html | strip_newlines %}
 {% assign test = test_bib | append: content | strip_html | strip_newlines %}
 {% if test == "" %}{% assign card-col-class = " col-md-offset-4" %}{% endif %}

_people/ayoun.md

+---
+firstname: Sacha
+lastname: Ayoun
+position: PhD Student
+webpage: https://www.doc.ic.ac.uk/~sja3417/
+email: s.ayoun17@imperial.ac.uk
+github:  https://github.com/Giltho/
+alumnus: false
+projects:
+  - gillian
+  - sl
+---
+Sacha Ayoun is a PhD student at the Department of Computing at Imperial, under
+the supervision of Professor Philippa Gardner. He is currently working 
+on [Gillian](https://gillianplatform.github.io), a parametric symbolic execution 
+tool for symbolic testing, verification and automatic compositional testing.
+
+As an undergraduate, Sacha worked at the [French Alternative and Atomic Energy Commission
+(CEA)](http://www.cea.fr/english) as a researcher-engineer intern in 2017. His goal was 
+to improve the Frame-C abstract interpreter to better handle file descriptors. 
+In 2018 he completed his Supelec Engineer Diploma at [CentraleSupelec](http://www.centralesupelec.fr/)
+as well as his MSc in Advanced Computing at Imperial.

_people/bodin.md

 ---
-
 firstname: Martin
 lastname: Bodin
-position: Research Associate
-webpage:  
-email: m.bodin@imperial.ac.uk
-github:  
-alumnus: false
+position: Researcher
+webpage: https://mbodin.github.io/index.html?lang=en&pedanticJS=no#en
+email: mbodin@ic.ac.uk
+github:
+alumnus: true
 projects:
   - web
 ---
-Martin Bodin is a Research Associate with the group. Martin Bodin did his PhD at 
-the [University of Rennes 1](https://english.univ-rennes1.fr/) under the supervision 
-of [Alan Schmitt]( http://people.rennes.inria.fr/Alan.Schmitt/index.html) 
-and [Thomas Jensen]( https://www.researchgate.net/profile/Thomas_Jensen3). 
-He participated to the [JSCert project]( http://www.jscert.org/) to build a Coq 
-specification for JavaScript. He applied the same formalising technique to build 
-a semantics for R during his postdoc at the [University of Chile]( http://www.cmm.uchile.cl/). 
-These specifications come with a high degree of confidence, but also with a large size. 
-His current work focuses on building and proving abstract analyses for such large semantics.
\ No newline at end of file
+Martin joined the group as a Research Associate in 2018. His work focused on a formalism called [skeletons](http://skeletons.inria.fr) to represent the semantics of real-world programming languages (JavaScript, R, etc.) He also was part of the team working on the [formalisation of WebAssembly/Wasm in Coq](https://github.com/Imperial-Wasm/wasm-coq-public). In 2020 Martin was appointed CRCN (chargé de recherche de classe normale) in the [Sound Programming of Adaptive Dependable Embedded Systems (Spades)](https://team.inria.fr/spades/) group at [Inria Grenoble-Rhône-Alpes Research Centre](https://www.inria.fr/en/centre-inria-grenoble-rhone-alpes), France.
\ No newline at end of file

_people/cerone.md

 ---
 firstname: Andrea
 lastname: Cerone
-position: Research Associate
-webpage: https://www.doc.ic.ac.uk/~acerone/
-email: a.cerone@imperial.ac.uk
+position: Researcher
 github: acerone85
-alumnus: false
+alumnus: true
 projects:
   - concurrency
   - moc
 ---
 
-Andrea Cerone is a Research Associate with the group. Andrea's research focuses on investigating the the mathematical foundations 
-of geo-replicated and distributed systems, with a particular emphasis to databases, and its applications for overcoming practical challenges in such systems.
\ No newline at end of file
+Andrea joined the group as a Research Associate in 2016. He left Imperial College in 2019,
+to move to industry. He is still an active researcher, continuing his work on the mathematical foundations 
+of geo-replicated and distributed systems, with a particular emphasis to databases, 
+and its applications for overcoming practical challenges in such systems.
+His latest publication is [Data Consistency in Transactional Storage Systems: 
+A Centralised Semantics](https://2020.ecoop.org/details/ecoop-2020-papers/21/Data-Consistency-in-Transactional-Storage-Systems-A-Centralised-Semantics) 
+at [Ecoop 2020](https://2020.ecoop.org/)

_people/d-osualdo.md

 ---
 firstname: Emanuele
 lastname: D'Osualdo
-position: Research Associate
+position: Researcher
 webpage: http://www.emanueledosualdo.com/
 email: e.dosualdo@imperial.ac.uk
 github: bordaigorl
-alumnus: false
+alumnus: true
 projects:
   - concurrency
-redirect_from: /people/dosualdo.html
 ---
 
-Emanuele D'Osualdo is a Research Associate with the group. His research interests include Semantics, 
-Models of Concurrency, Static Analysis, Process Algebra, Security, 
-Abstract Interpretation, Model Checking, Programming Languages, Declarative Programming.
+Emanuele joined the group as a Marie-Curie Fellow in 2018 with his project [“Verification through Security and Progress Abstractions” (VeSPA)](https://www.emanueledosualdo.com/blog/2018/announce-marie-curie-fellowship.html). In 2020 he moved to the [Max Planck Institute for Software Systems (MPI-SWS)](https://www.mpi-sws.org/research-areas/programming-languages-and-verification/), Germany, to work on the verification of concurrent programs with the [IRIS program logic](https://iris-project.org/) project.
\ No newline at end of file