.deploy.sh

@@ -10,5 +10,5 @@ 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 --chmod=Dg+s,ug+rwX,o+rX --chown=:rr -igrp --delete _site/ "${USER}${SERVER}:${PTH}"
+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,7 +3,7 @@ stages:
   - build
   - deploy
 
-image: "ruby:2"
+image: "ruby:2.6-buster"
 variables:
   NOKOGIRI_USE_SYSTEM_LIBRARIES: "true"
 
@@ -20,6 +20,7 @@ build:
     - triggers
   tags:
     - docker
+    - vtss_site
   before_script:
     - bundle install --deployment --without=development --with=test
     - bundle exec rake init
@@ -36,6 +37,7 @@ deadlinks:
     - triggers
   tags:
     - docker
+    - vtss_site
   before_script:
     - bundle install --deployment --without=development --with=test
   script:
@@ -47,6 +49,7 @@ deploy:
   image: resourcereasoning/website-deploy
   tags:
     - docker
+    - vtss_site
   only:
     - master
   except:
@@ -71,6 +74,7 @@ update_publications:
   image: ignoredambience/github-gitlab-sync
   tags:
     - docker
+    - vtss_site
   only:
     - triggers
   before_script:

.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

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

_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
 

_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 }}<br />
-  <a href="https://www.imperial.ac.uk/about-the-site/privacy/">Privacy Notice</a></p>
+  <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

@@ -7,15 +7,16 @@ email: s.ayoun17@imperial.ac.uk
 github:  https://github.com/Giltho/
 alumnus: false
 projects:
-  - web
-  - moc
+  - gillian
+  - sl
 ---
-Sacha Ayoun is a PhD student at the Department of Computing at Imperial, under 
-the supervision of Professor Philippa Gardner. During his undergraduate 2017, 
-he worked at the [French Alternative and Atomic Energy Commission 
-(CEA)](http://www.cea.fr/english) as a researcher-engineer intern. 
-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.  His PhD will be focused 
-on JavaScript Verification using separation logic.
\ No newline at end of file
+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

_people/da-rocha-pinto.md

@@ -10,4 +10,4 @@ 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]({{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.
+He is currently working for [Collage.com, Inc.](https://www.collage.com/) a Michigan-based photo products e-commerce company.
\ No newline at end of file

_people/fragoso-santos.md

 ---
 firstname: José
 lastname: Fragoso Santos
-position: Research Associate
-webpage: http://www.doc.ic.ac.uk/~jfaustin/
-email: jose.fragoso.santos@imperial.ac.uk
+position: Researcher
+webpage: http://web.ist.utl.pt/jose.fragoso/
+email: jose.fragoso@tecnico.ulisboa.pt
 github: j3fsantos
-alumnus: false
+alumnus: true
 projects:
-  - web
-  - sl
-  - infer
+  - gillian
 ---
 
-Jose Fragoso is a Research Associate with the group, working on  program analysis, verification, and instrumentation, with applications to security.
\ No newline at end of file
+José joined the group as a Research Associate in 2015, working on
+program analysis and JavaScript Verification. He is now an Assistant Professor
+at the Instituto Superior Técnico, Lisbon, Portugal.
\ No newline at end of file

_people/gardner.md

@@ -11,19 +11,25 @@ projects:
   - sl
   - moc
   - infer
+  - gillian
 ---
-Philippa Gardner is a professor in the [Department of Computing](http://www.doc.ic.ac.uk) at Imperial
-and leader of the Verified Trustworthy Software Specification Group. 
-Her current research focusses on program verification: in particular, reasoning about Web programs 
-(JavaScript and DOM) and reasoning about concurrent programs.
+Philippa Gardner is a professor in the [Department of Computing](https://www.doc.ic.ac.uk/) at [Imperial College London](https://www.imperial.ac.uk/)
+and has a UK Research and Innovation [Established Fellowship](https://gtr.ukri.org/projects?ref=EP%2FR034567%2F1) from 2018-2023.
+Her research focusses on program specification and verification. In particular,
+her group is credited with bringing logical abstraction and logical atomicity to
+modern concurrent separation logics, and is currently developing the Gillian
+platform for building symbolic  analysis tools for real-world programming languages
+such as C and JavaScript, which unifies classical symbolic execution, semi-automatic
+verification based on separation logic, and automatic compositional testing based
+on bi-abduction.
 
-She completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992. She moved to Cambridge in 1998 
-on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. 
-She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of
-Engineering Senior Fellowship from 2005 to 2010 at Imperial. She was the  Director 
-of the [Research Institute in Automated Program Analysis and Verification](http://www.verificationinstitute.org),
-funded by GCHQ in association  with EPSRC from 2013 to 2017.
+Gardner completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at
+Edinburgh in 1992 and held five years of fellowships at Edinburgh. She moved to
+Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS.
+She obtained a lectureship at Imperial in 2001, and became professor in 2009.
+She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior
+Fellowship at Imperial, 2005-2009. 
 
-Philippa directs the [Research Institute on Verified Trustworthy Software Systems (VeTSS)](https://vetss.org.uk/), 
-funded by EPSRC, from 2017 to 2022. She also chairs the BCS awards committee, 
-which decides the [Lovelace medal](http://www.bcs.org/category/5932) (senior) and [Roger Needham award](http://www.bcs.org/category/5941) (mid-career) for computer science and engineering.
+Philippa directs the [Research Institute on Verified Trustworthy Software Systems (VeTSS)](https://vetss.org.uk/),
+funded by EPSRC and NCSC, 2017-2022. She is an organiser
+of the [Isaac Newton Institute six-week summer programme on `Verified Software', 2022](https://www.newton.ac.uk/event/vso2/). In 2020 she was elected a [Fellow of the Royal Academy of Engineering](https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2020/fellows/professor-philippa-gardner).

_people/karmios.md

+---
+firstname: Nat
+lastname: Karmios
+position: Researcher
+webpage: 
+email: nathaniel.karmios18@imperial.ac.uk
+github: 
+alumnus: false
+projects:
+---
+
+Nat Karmios is a Research Engineer in Imperial's Verified Software Group under Professor Philippa Gardner, working on [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html), a parametric symbolic execution tool for symbolic testing, verification and automatic compositional testing.
+
+After earning their MEng in Computing at Imperial - completing their thesis project with the group - Nat has brought their years of industry engineering experience to improve Gillian's accessibility through the development of a visual debugger for symbolic execution and verification.

_people/loow.md

+---
+firstname: Andreas
+lastname: Lööw
+position: Researcher
+webpage: https://www.doc.ic.ac.uk/~aloow/
+email: a.loow@imperial.ac.uk
+github: https://github.com/AndreasLoow
+alumnus: false
+projects:
+---
+
+Andreas did his PhD at Chalmers University of Technology, in Sweden, under the supervision of [Magnus Myreen](http://www.cse.chalmers.se/~myreen/). At Chalmers, Andreas worked on interactive theorem proving for software and hardware correctness. Specifically, he worked on building trustworthy computer systems, known as verified stacks, with full-system correctness theorems. Much of his work revolved around trustworthy hardware, for example in the form of the development and verification of the [Verilog synthesis tool Lutsig](https://dl.acm.org/doi/10.1145/3437992.3439916). Andreas defended his thesis, [Building Verified Hardware and Verified Stacks in HOL](https://www.doc.ic.ac.uk/~aloow/papers/thesis.pdf), in September 2021.

_people/maksimovic.md

 ---
 firstname: Petar
 lastname: Maksimović
-position: Research Fellow
+search_lastname: Maksimovic
+position: Researcher
 webpage: https://sites.google.com/site/petarmaksimovic1981/
 email: p.maksimovic@imperial.ac.uk
 github: PetarMax
-alumnus: false
+alumnus: true
 projects:
   - web
   - moc
   - sl
+  - gillian
 ---
 
-Petar Maksimović is a Research Fellow with the group and the Academic Program Manager for the [Research Institute on Verified Trustworthy Software Systems (VeTSS)](https://vetss.org.uk/). 
+Petar Maksimović was a Research Fellow with the group and the Academic Program Manager for the [Research Institute on Verified Trustworthy Software Systems (VeTSS)](https://vetss.org.uk/) until his move to industry in 2022.
 
-He also holds the position of Research Assistant Professor at the Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade.
\ No newline at end of file
+Petar is also a Research Assistant Professor at the Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade.

_people/nantes.md

+---
+firstname: Daniele
+lastname: Nantes
+position: Researcher
+webpage: 
+email: d.nantes-sobrinho@imperial.ac.uk
+github:  
+alumnus: false
+projects:
+---
+
+[Daniele](https://mat.unb.br/dnantes/) is a tenured assistant professor at the Department of Mathematics, University of Brasília, and is currently in a long sabbatical leave. 
+
+Daniele's research focusses on equational reasoning and comparative expressiveness of models and languages with concurrency.  She was a researcher with the [Theoretical Computer Science Group (GTC-UnB)](https://www.mat.unb.br/ayala/TCgroup/index.html), and an external collaborator of the [VIDI project Unifying Correctness for Communicating Systems](https://www.jperez.nl/vidi). Her latest publications are [Formalising nominal C-unification generalised with protected variables](https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/formalising-nominal-cunification-generalised-with-protected-variables/0299ECF29C28FDD65AAE38E73BF28FE3), published in Mathematical Structures for Computer Science, and the conference papers [Nominal Equational Problems](https://link.springer.com/chapter/10.1007/978-3-030-71995-1_2), published in ETAPS’ Foundations of Software Science and Computation Structures (FOSSACS 2021) series, and [Non-deterministic Functions as Non-Deterministic Processes](https://drops.dagstuhl.de/opus/volltexte/2021/14259/), in Formal Structures for Computation and Deduction (FSCD 2021) series.