.gitlab-ci.yml

@@ -3,7 +3,7 @@ stages:
   - build
   - deploy
 
-image: "ruby:2.6-stretch"
+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
+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>

_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
+position: Researcher
 github: acerone85
 alumnus: true
 projects:
@@ -9,10 +9,10 @@ projects:
   - moc
 ---
 
-Andrea moved to industry in 2019. He is still an active researcher, continuing 
-his work on the mathematical foundations 
+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/)
\ No newline at end of file
+at [Ecoop 2020](https://2020.ecoop.org/)

_people/d-osualdo.md

 ---
 firstname: Emanuele
 lastname: D'Osualdo
-position: Marie-Curie Fellow
+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 Marie-Curie Fellow in Theoretical Computer Science, 
-at Imperial College London, working with Philippa Gardner. His research interests 
-include Semantics, Models of Concurrency, Static Analysis, Process Algebra, Security, 
-Abstract Interpretation, Model Checking, Programming Languages, Declarative Programming.
\ No newline at end of file
+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/fragoso-santos.md

 ---
 firstname: José
 lastname: Fragoso Santos
-position: Research Associate
+position: Researcher
 webpage: http://web.ist.utl.pt/jose.fragoso/
 email: jose.fragoso@tecnico.ulisboa.pt
 github: j3fsantos
 alumnus: true
 projects:
-  - web
-  - sl
-  - infer
+  - gillian
 ---
 
-José joined the group as a Research Associate in 2015, working on 
-program analysis and JavaScript Verification. He is now an Assistant Professor 
+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,24 +11,25 @@ projects:
   - sl
   - moc
   - infer
+  - gillian
 ---
 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 
+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.
 
-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 
+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 and NCSC, 2017-2022. She is an organiser 
-of the [Isaac Newton Institute six-week summer programme on `Verified Software', 2020](http://www.newton.ac.uk/event/vso).
\ No newline at end of file
+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

@@ -2,17 +2,18 @@
 firstname: Petar
 lastname: Maksimović
 search_lastname: Maksimovic
-position: Research Fellow
+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.

_people/naudziuniene.md

@@ -2,10 +2,10 @@
 firstname: Daiva
 lastname: Naudžiūnienė
 search_lastname: Naudziuniene
-position: PhD Student   
+position: PhD Student
 alumnus: true
 ---
 
-Daiva defended her Ph.D. on [An Infrastructure for Tractable Verification of JavaScript Programs]({{site.baseurl}}{% link publications/Naudziuniene2018Infrastructure.html %}) in March 2018.   
+Daiva defended her PhD on [An Infrastructure for Tractable Verification of JavaScript Programs]({{site.baseurl}}{% link publications/Naudziuniene2018Infrastructure.html %}) in March 2018.
 
-Since 2017 Daviva has been working as a Research Scientist at Facebook as part of the engineering team led by Peter O’Hearn.
\ No newline at end of file
+Since 2017, Daiva has been working as a Research Scientist at Facebook as part of the engineering team led by Peter O’Hearn.

_people/raad.md

@@ -8,7 +8,7 @@ alumnus: true
 ---
 
 Azalea was a PhD student with the group, defending her thesis on [Abstraction, Refinement and Concurrent Reasoning]({{site.baseurl}}{% link publications/Raad2017Abstraction.html %}) in February 2017.
-She then moved to the [Max Planck Institute for Software Systems (Kaiserslautern)](https://www.mpi-sws.org/) 
+She then moved to the [Max Planck Institute for Software Systems (Kaiserslautern)](https://www.mpi-sws.org/)
 working a postdoctoral researcher with [Derek Dreyer](https://people.mpi-sws.org/~dreyer/) and [Viktor Vafeiadis](https://people.mpi-sws.org/~viktor/)
-on the [ERC RustBelt project](http://plv.mpi-sws.org/rustbelt/). In 2020 Azalea joined the faculty 
+on the [ERC RustBelt project](http://plv.mpi-sws.org/rustbelt/). In 2020, Azalea joined the faculty
 at Imperial College London as a lecturer.
\ No newline at end of file

_people/rao.md

+---
+firstname: Xiaojia
+lastname: Rao
+position: PhD Student
+webpage: 
+email: xiaojia.rao19@imperial.ac.uk
+github:  
+alumnus: false
+projects:
+  - gillian
+  - sl
+---
+
+Xiaojia is a PhD student at the Department of Computing at Imperial, under the supervision of Professor Philippa Gardner.
+
+Xiaojia studied for his BA and Math degree at the University of Cambridge and then moved to Imperial College London in 2020 to join the MSc in Advanced Computing. His Master's thesis was on a verified model of WebAssembly in Coq called WasmCert-Coq. He plans to expand this work, and also explore the Iris framework and [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html) in his future research.
\ No newline at end of file