.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

_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>

_people/ayoun.md

@@ -15,9 +15,8 @@ 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.
 
-During his undergraduate 2017, Sacha 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.
\ No newline at end of file
+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

@@ -3,15 +3,10 @@ firstname: Martin
 lastname: Bodin
 position: Researcher
 webpage: https://mbodin.github.io/index.html?lang=en&pedanticJS=no#en
-email: m.bodin@imperial.ac.uk
+email: mbodin@ic.ac.uk
 github:
 alumnus: true
 projects:
   - web
 ---
-Martin Bodin was a Research Associate with the group. In 2020 Martin joined the [Inria Grenoble-Rhône-Alpes Research Centre](https://www.inria.fr/en/centre-inria-grenoble-rhone-alpes) as a CRCN (chargé de recherche de classe normale) with the [Sound Programming of Adaptive Dependable Embedded Systems (Spades)](https://team.inria.fr/spades/) group. 
-
-While at Imperial, Martin's work focused on a formalism called skeletons used to represent the semantics
-of real-world language, in order to get as many properties as possible [certified in the Coq
-proof assistant](https://coq.inria.fr). He also was part of the team working on the 
-[formalisation of WebAssembly/Wasm in Coq](https://github.com/Imperial-Wasm/wasm-coq-public).
\ 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

@@ -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

@@ -10,4 +10,4 @@ projects:
   - concurrency
 ---
 
-Emanuele D'Osualdo 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
+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/gardner.md

@@ -28,8 +28,8 @@ 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.
+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
+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

@@ -6,7 +6,7 @@ position: Researcher
 webpage: https://sites.google.com/site/petarmaksimovic1981/
 email: p.maksimovic@imperial.ac.uk
 github: PetarMax
-alumnus: false
+alumnus: true
 projects:
   - web
   - moc
@@ -14,6 +14,6 @@ projects:
   - 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

@@ -6,6 +6,6 @@ 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, Daiva 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/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

_people/sampaio.md

@@ -3,18 +3,13 @@ firstname: Gabriela
 lastname: Sampaio
 position: PhD Student
 webpage: https://www.doc.ic.ac.uk/~gcs817/
-email: g.sampaio17@imperial.ac.uk
+email:
 github:  
-alumnus: false
+alumnus: true
 projects:
   - web
   - moc
 ---
-Gabriela Sampaio is a PhD student at the [Department of Computing](http://www.doc.ic.ac.uk) at
+Gabriela Sampaio was a PhD student at the [Department of Computing](http://www.doc.ic.ac.uk) at
 Imperial, under the supervision of Professor Philippa Gardner. 
-She completed her BSc course at Federal University of Pernambuco (UFPE, Brazil) in 2015. 
-During the undergraduate course, she spent one year at the University of Kent, working on an Erlang refactoring project ([Wrangler](https://www.cs.kent.ac.uk/projects/wrangler/Wrangler/Home.html)) 
-under the supervision of Professor Simon Thompson. Later in 2017, she completed her MSc, also at UFPE, under supervision of Professor Paulo Borba. 
-The work aims to support developers in partially safe changes to software product lines, with the use of a partial refinement theory. 
-The results were published at [SPLC'16](https://dl.acm.org/citation.cfm?id=2934482). Between the MSc and the PhD, Gabriela worked as a web developer in Brazil. 
-Her PhD thesis will focus on the reasoning and verification of large Javascript Programs.
+She completed her BSc  and MSc at Federal University of Pernambuco (UFPE, Brazil), spending a year abroad at the University of Kent, working on the Erlang refactoring project ([Wrangler](https://www.cs.kent.ac.uk/projects/wrangler/Wrangler/Home.html)). In 2022, Gabriela defended her PhD thesis, [A Trusted Infrastructure for Symbolic Analysis of Event based Web APIS](https://spiral.imperial.ac.uk/bitstream/10044/1/100397/1/CunhaSampaio-G-2022-PhD-Thesis.pdf), and took up a position at Meta (formerly Facebook).

_people/sutherland.md

@@ -3,12 +3,11 @@ firstname: Julian
 lastname: Sutherland
 position: PhD Student
 webpage: http://www.doc.ic.ac.uk/~jhs110/
-email: jhs110@doc.ic.ac.uk
-alumnus: false
+email: 
+alumnus: true
 projects:
   - concurrency
   - sl
 ---
 
-Julian is a PhD student with the group, currently working on extending 
-concurrent separational logics such as TaDA to a total correctness semantics (termination).
+Julian defended his PhD thesis, Compositional termination verification for fine-grained concurrency, in 2022. Julian is currently a Formal Verification Engineer at [Nethermind](https://nethermind.io/), a blockchain company working on Ethereum.

_people/xiong.md

@@ -11,7 +11,6 @@ projects:
   - moc
 ---
 
-Shale was a PhD student with the group. Shale defended his thesis: Parametric Operational 
-Semantics for Consistency Models in February 2020 and he is currently working 
-for [Arm Research]( https://www.arm.com/resources/research), Cambridge, as a 
-Research Engineer in their Security group.
\ No newline at end of file
+Shale was a PhD student with the group. Shale defended his thesis: [Parametric Operational 
+Semantics for Consistency Models](https://vtss.doc.ic.ac.uk/publications/Xiong2020Parametric.html) in February 2020 and he is currently working for [Arm Research](https://www.arm.com/resources/research), Cambridge, as a 
+Research Engineer in their Security group.

_posts/2020-09-27-fellow.md

+---
+title: Congratulations to Philippa Gardner, elected Fellow of the RAEng 
+--- 
+
+Philippa was one of 53 engineers in the UK to be elected to the Fellowship of the Royal Academy of Engineering this year. 
+
+Becoming a [Fellow of the RAEng]( https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2020/fellows/professor-philippa-gardner) is one of the highest honors an engineer can receive in the UK, and it recognizes outstanding and continuing contributions to the profession. 
+
+After the announcement, Philippa expressed her hope that her work "will serve as a foundation for establishing trust in our modern software infrastructure” and thanked her the group, for what she described as a “real group achievement, not just my achievement"
\ No newline at end of file

_posts/2020-10-01-martin.md

 ---
-title: Goodbye and best of luck to Martin Bodin
+title: Goodbye to Martin Bodin
 ---
 
 Goodbye and our best wishes to Martin Bodin who is leaving the group to join [the Inria Grenoble-Rhône-Alpes Research Centre](https://www.inria.fr/en/centre-inria-grenoble-rhone-alpes), France, as a CRCN (chargé de recherche de classe normale) in the [Sound Programming of Adaptive Dependable Embedded Systems (Spades)](https://team.inria.fr/spades/) group.
 
-The Spades group’s research focuses on component-based programming: analysis of embedded systems, both in term of correctness and efficiency (time or energy use) and Martin will work in particular on the topic of Skeletal Semantics as Certified Analyses of Real-world Programs. You can read more about his proposed research below.
+Ni deziras al vi bonŝancon en via nova posto ĉe Inria, Martin!
 
-Many programming languages used in industry are complex. This complexity is sometimes associated to deep research questions, like pointer arithmetic or concurrency. However, this complexity is sometimes only due to special behaviours of these languages. Languages likes JavaScript or R are known for such unexpected special behaviours. Such programming languages are thus frequently idealised in research. This unfortunately narrows the application of formal analyses. My research aims at developing formalisms (namely, skeletal semantics in the context of the Coq proof assistant) that enable the application of analyses of such complex languages, in particular in the context of real-time systems.
+The Spades group’s research focuses on component-based programming: analysis of embedded systems, both in term of correctness and efficiency (time or energy use) and Martin will work in particular on the topic of Skeletal Semantics as Certified Analyses of Real-world Programs. You can read more about his proposed research below.
 
-Ni deziras al vi bonŝancon en via nova posto ĉe Inria, Martin!
+Many programming languages used in industry are complex. This complexity is sometimes associated to deep research questions, like pointer arithmetic or concurrency. However, this complexity is sometimes only due to special behaviours of these languages. Languages likes JavaScript or R are known for such unexpected special behaviours. Such programming languages are thus frequently idealised in research. This unfortunately narrows the application of formal analyses. My research aims at developing formalisms (namely, skeletal semantics in the context of the Coq proof assistant) that enable the application of analyses of such complex languages, in particular in the context of real-time systems.
\ No newline at end of file