Compare revisions

b253ece8 · 6a324a61 · 6b1386fb · 24171d0b · 464ba1d1 · 4c36de4f
--- a/.deploy.sh
+++ b/.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}"
+
--- a/.gitignore
+++ b/.gitignore
@@ -3,3 +3,4 @@ _site
 .jekyll-metadata
 vendor
 .bundle/config
+.DS_Store
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
 stages:
  - update
-  - test
+  - 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\n\n[ci skip]" || 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"

-test:
-  stage: test
-  image: "ruby:2.4"
+build:
+  stage: build
+  artifacts:
+    paths:
+      - _site/
+    expire_in: 1 day
+  cache:
+    paths:
+      - vendor/bundle/
+  except:
+    - triggers
  tags:
    - docker
+    - vtss_site
  before_script:
-    - bundle install --without=development
+    - 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

 deadlinks:
  stage: deploy
-  image: "ruby:2.4"
+  allow_failure: true
+  cache:
+    paths:
+      - vendor/bundle/
+  except:
+    - triggers
  tags:
    - docker
+    - vtss_site
  before_script:
-    - bundle install --without="build development" --with=test
+    - bundle install --deployment --without=development --with=test
  script:
    - bundle exec rake -s --suppress-backtrace . testlinks
-  allow_failure: true

 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"
+# 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}
--- a/.gitmodules
+++ b/.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
--- 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
--- a/Dockerfile
+++ b/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
--- a/Gemfile
+++ b/Gemfile
 source 'https://rubygems.org'

+Encoding.default_external = Encoding::UTF_8
+
 gem 'rake'
 group :build do
  gem 'jekyll'

--- a/Gemfile.lock
+++ b/Gemfile.lock
 GEM
  remote: https://rubygems.org/
  specs:
-    activesupport (5.1.3)
+    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.1)
-      public_suffix (~> 2.0, >= 2.0.2)
-    bibtex-ruby (4.4.4)
+    addressable (2.5.2)
+      public_suffix (>= 2.0.2, < 4.0)
+    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)
-    colored (1.2)
-    concurrent-ruby (1.0.5)
-    csl (1.4.5)
-      namae (~> 0.7)
-    csl-styles (1.0.1.8)
+    colorize (0.8.1)
+    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.2)
+    html-proofer (3.9.2)
      activesupport (>= 4.2, < 6.0)
      addressable (~> 2.3)
-      colored (~> 1.2)
+      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.5.2)
+    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)
-      kramdown (~> 1.3)
+      jekyll-watch (~> 2.0)
+      kramdown (~> 1.14)
      liquid (~> 4.0)
      mercenary (~> 0.3.3)
      pathutil (~> 0.9)
-      rouge (~> 1.7)
+      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.14.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.2.0)
-    minitest (5.10.3)
-    namae (0.11.3)
-    nokogiri (1.8.0)
-      mini_portile2 (~> 2.2.0)
-    parallel (1.12.0)
-    pathutil (0.14.0)
+    mini_portile2 (2.3.0)
+    minitest (5.11.3)
+    namae (1.0.1)
+    nokogiri (1.8.5)
+      mini_portile2 (~> 2.3.0)
+    parallel (1.12.1)
+    pathutil (0.16.2)
      forwardable-extended (~> 2.6)
-    public_suffix (2.0.5)
-    rake (12.0.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 (1.11.1)
+    rouge (3.3.0)
+    ruby_dep (1.5.0)
    safe_yaml (1.0.4)
-    sass (3.5.1)
+    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.3
+   1.16.6
--- a/README.md
+++ b/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
@@ -55,6 +55,35 @@ Any other files present in the directory structure (except for those prefixed wi

 For the detail of adding publication, please refer to the README file in publication directory.

+Jekyll Scholar Configuration Detail
+===================================
+We desire the output URL structure to be:
+* `/publications/`
+  * `index.html` - a page listing the entire bibliography
+  * `publications.bib` - the raw bibtex file, directly from the source
+  * `Key.html` - details page generated for each publication
+  * `Key.*` - Any files associated with each publication, copied directly from the source
+
+In the `scholar` section of the configuration file, configuration options we've used are:
+* `source`: Directory in which our bibtex files are to be found (`publications`)
+* `details_dir`: Directory to output `Key.html` files for each publication (`publications`), rendered using the layout
+  defined in the `details_layout` option.
+* `details_link`: We override the default here, as we generate our own HTML to render this link in our
+  `bibliography_template`.
+* `repository`: Location of files associated with publications (`publications`) (the same
+  directory is used for both input and output: it is handled as usual by jekyll)
+
+The template used to generate individual publication pages is [here](_layouts/publication.html). The part of interest is
+the Source Materials section. We iterate through a
+[predefined list of file types](publications/_publication_file_types.yml) and output a link (using icon and text from
+the file type list) to the file in the repository if it exists.
+
+Finally, in order to generate the complete biography page, we use a [page](publications.html) in the site's root just
+outputting a `{% bibliography %}` as normal (which renders each entry using the layout defined by the scholar
+`bibliography_template` option). By using a `permalink` jekyll option we place the rendered bibliography into the
+`/publications/` output directory as `index.html`.
+
+
 Testing and Deployment
 ----------------------
 The DoC GitLab instance is configured (using .gitlab-ci.yml) to build, test and deploy the website on tests passing.
@@ -64,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
 ----------------------------

--- a/Rakefile
+++ b/Rakefile
@@ -15,7 +15,8 @@ end
 htmlproofer_config = {
  :disable_external => true,
  :check_html => true,
-  :parallel => { :in_processes => 1 }
+  :parallel => { :in_processes => 1 },
+  :file_ignore => [/README.html/]
 }

 desc "Build the site and test output for dead links, invalid html etc."
@@ -34,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
--- a/_config.yml
+++ b/_config.yml
-title: Program Specification and Verification 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:
@@ -14,6 +17,7 @@ exclude:
  - Rakefile
  - .gitlab-ci.yml
  - vendor
+  - publications/README.md

 collections:
  people:

--- a/_data/external_assets.yml
+++ b/_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
--- a/_includes/alumni.html
+++ b/_includes/alumni.html
+<div class="people panel">
+
+  {% assign grouped_people = include.people | group_by: 'position' | sort: 'name' %}
+  {% for group in grouped_people %}
+  {% assign position = group.name %}
+  {% assign id = group.name | replace:' ','-' %}
+  <div class="panel-heading">
+    <h6 class="panel-title">
+      <a data-toggle="collapse" href="#{{id}}" style="color:black">{{position}}s ↯</a>
+    </h6>
+  </div>
+
+  <div id="{{id}}" class="panel-collapse collapse">
+    {% for person in group.items %}
+    <div class="row">
+      <div class="col-sm-1" >
+        <a href="{{ person.url }}" >{% include person-photo-small.html %}</a>
+      </div>
+      <div class="col-sm-11">
+        <a href="{{ person.url }}" class="h6" style="color:black;font-weight:bold;">{{ person.firstname }} {{ person.lastname }}</a>
+        {{ person.content | remove: '<p>' | remove: '</p>' }}
+      </div>
+    </div>
+    <br/>
+    {% endfor %}
+  </div>
+  {% endfor %}
+</div>
--- a/_includes/footer.html
+++ b/_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>
--- a/_layouts/home.html
+++ b/_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>

--- a/_layouts/person.html
+++ b/_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 %}

--- a/_people/ayoun.md
+++ b/_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.
--- a/_people/bodin.md
+++ b/_people/bodin.md
+---
+firstname: Martin
+lastname: Bodin
+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 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
--- a/_people/cerone.md
+++ b/_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: true
 projects:
  - concurrency
  - moc
 ---
+
+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/)
--- a/_people/d-osualdo.md
+++ b/_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: true
 projects:
  - concurrency
-redirect_from: /people/dosualdo.html
 ---
+
+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
No results found