_people/da-rocha-pinto.md

@@ -7,7 +7,7 @@ email: pmd09@doc.ic.ac.uk
 github: pedromdrp
 alumnus: true
 ---
-Pedro da Rocha Pinto was a [PhD student and a Post Doc](https://www.doc.ic.ac.uk/~pmd09/) with the group from 2010 to 2016, 
-working on developing logics for verification of fine-grained concurrent programs.
-Pedro defended his PhD thesis, [Reasoning with Time and Data Abstractions](https://psvg.doc.ic.ac.uk/publications/daRochaPinto2017Reasoning.html) in January 2017.
-He is currently working for [Enki Labs Inc.](http://www.enkilabs.com/) and in the process of starting his own company, Alfarroba.
\ No newline at end of file
+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.
\ 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
 ---
+
+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 Program Specification and Verification 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), 
-funded by EPSRC, from 2017 to 2022. She also chairs the BCS awards committee, 
-which decides the Lovelace medal (senior) and Roger Needham award (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ć 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.
+
+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

 ---
 firstname: Daiva
 lastname: Naudžiūnienė
-position: PhD Student   
-webpage: http://www.doc.ic.ac.uk/~dn911/
-email: d.naudziuniene11@imperial.ac.uk
+search_lastname: Naudziuniene
+position: PhD Student
 alumnus: true
 ---
-Daiva submitted her Ph.D. on An Infrastructure for Tractable Verification of JavaScript Programs in September 2017; the viva will take place in March 2018.
-From 2017 Daviva has been working as a Reseaarch Scientist at Facebook as part of the engineering team led by Peter O’Hearn. 
\ No newline at end of file
+
+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.

_people/ntzik.md

@@ -2,10 +2,10 @@
 firstname: Gian
 lastname: Ntzik
 position: PhD Student
-webpage: http://www.doc.ic.ac.uk/~gn408/
-email: gian.ntzik08@imperial.ac.uk
 github: anirothan
 alumnus: true
-projects:
 ---
 
+Gian was a PhD student and Post Doc with the group. Gian defended his thesis [Reasoning about POSIX File Systems]({{site.baseurl}}{% link publications/Ntzik2017Reasoning.html %}) 
+in February 2017 and is currently working for [Amadeus](http://www.amadeus.com/web/amadeus/en_GB-GB/Amadeus-Home/About-us/Our-company/1319477448520-Page-AMAD_DetailPpal) 
+in systems development and research.
\ No newline at end of file

_people/raad.md

@@ -2,9 +2,13 @@
 firstname: Azalea
 lastname: Raad
 position: PhD Student
-webpage: http://www.doc.ic.ac.uk/~azalea/
+webpage: http://www.soundandcomplete.org/
 email: azalea@imperial.ac.uk
 alumnus: true
-projects:
 ---
 
+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/)
+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
+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

_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, course 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,10 +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 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/wood.md

@@ -2,11 +2,9 @@
 firstname: Thomas
 lastname: Wood
 position: PhD Student
-webpage: http://www.doc.ic.ac.uk/~tw1509/
-email: tw1509@doc.ic.ac.uk
-github: edgemaster
-alumnus: false
-projects:
-  - web
+webpage: https://twitter.com/IgnoredAmbience
+github: IgnoredAmbience
+alumnus: true
 ---
 
+Thomas was a PhD student with the group, working on software automated testing, verification and reasoning techniques and theory.
\ No newline at end of file

_people/xiong.md

@@ -5,9 +5,12 @@ position: PhD Student
 webpage: http://www.doc.ic.ac.uk/~sx14/
 email: shale.xiong14@imperial.ac.uk
 github: ShaleXIONG
-alumnus: false
+alumnus: true
 projects:
   - concurrency
   - moc
 ---
 
+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/2016-10-03-papers.md

@@ -3,6 +3,6 @@ title: Papers published by Azalea Raad
 ---
 Azalea Raad has had two papers published in Programming Languages and System: Proceedings of the 14th Asian Symposium, [APLAS 2016](https://soict.hust.edu.vn/~aplas2016/).
 
-The papers are: [Verifying Concurrent Graph Algorithms](http://psvg.doc.ic.ac.uk/publications/Raad2016Verifying.html) (with Aquinas Hobor, Jules Villard and Philippa Gardner) and [DOM: Specification and Client Reasoning](http://psvg.doc.ic.ac.uk/publications/Raad2016DOM.html) (with José Fragoso Santos and Philippa Gardner).
+The papers are: [Verifying Concurrent Graph Algorithms](http://vtss.doc.ic.ac.uk/publications/Raad2016Verifying.html) (with Aquinas Hobor, Jules Villard and Philippa Gardner) and [DOM: Specification and Client Reasoning](http://vtss.doc.ic.ac.uk/publications/Raad2016DOM.html) (with José Fragoso Santos and Philippa Gardner).
 
-These and other group papers can be found on our [publications page](http://psvg.doc.ic.ac.uk/publications/).
+These and other group papers can be found on our [publications page](http://vtss.doc.ic.ac.uk/publications/).

_posts/2016-11-14-inferlab.md

@@ -2,7 +2,7 @@
 title: Infer Lab at Imperial
 ---
 
-The [Separation Logic](https://psvg.doc.ic.ac.uk/teaching/separationlogic.html) course team ran a lab on [Infer](http://fbinfer.com/), 
+The [Separation Logic]({{site.baseurl}}{% link teaching/separationlogic.md %}) course team ran a lab on [Infer](http://fbinfer.com/), 
 an automatic verification tool based on separation logic, developed at [Facebook](https://www.facebook.com/inferstaticanalyzer/) 
 where it is used every day to verify millions of lines of code.
 
@@ -19,4 +19,4 @@ During the tutorial, one of the students, Lorenzo Paoliani, ran Infer on Connect
 and found several null dereference bugs. He reported this on github and submitted a pull request for fixing that problem, 
 which has been accepted and now merged.
 
-For more details and slides, see the [Infer Lab 2016](https://psvg.doc.ic.ac.uk/teaching/InferLab.html) page.
\ No newline at end of file
+For more details and slides, see the [Infer Lab 2016]({{site.baseurl}}{% link teaching/InferLab.md %}) page.
\ No newline at end of file

_posts/2016-12-15-Dolby.md

@@ -3,11 +3,11 @@ title: Visit from Julian Dolby, IBM
 ---
 [Julian Dolby](http://researcher.watson.ibm.com/researcher/view.php?person=us-dolby), a researcher at IBM's 
 [Thomas J. Watson Research Center](http://www.research.ibm.com/labs/watson/index.shtml)
-in New York visited the PSVG group for a week in December.
+in New York visited the VTSS group for a week in December.
 
 Julian’s research focuses on static program analysis, 
 software testing and the semantic web and during his visit, Julian worked with José Fragoso and Petar Maksimovic 
-in a [symbolic analysis for JavaScript](https://psvg.doc.ic.ac.uk/research/javascript.html) 
+in a [symbolic analysis for JavaScript]({{site.baseurl}}{% link research/javascript.md %}) 
 based on JSIL and Rosette with the end goal of having a bug-finding tool for JavaScript.
 
 [ROSETTE](https://github.com/juliandolby/rosette) is a solver-aided programming language 

_posts/2017-01-13-Pedro_viva.md

@@ -10,6 +10,6 @@ and to [Susan Eisenbach](http://www.imperial.ac.uk/people/s.eisenbach), who acte
 
 Pedro’s thesis was about exploring a number of design possibilities for a logic for 
 modularly verifying shared-memory concurrent programs and introduces a new program logic 
-called [TaDA](https://psvg.doc.ic.ac.uk/publications/daRochaPinto2014TaDA.html) for verifying concurrent programs with much better support for abstraction.
+called [TaDA]({{site.baseurl}}{% link publications/daRochaPinto2014TaDA.html %}) for verifying concurrent programs with much better support for abstraction.
 
-Pedro's latest paper, accepted to ESOP 2017 is on [our publications page](https://psvg.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html).
+Pedro's latest paper, accepted to ESOP 2017 is on [our publications page]({{site.baseurl}}{% link publications/Dinsdale-Young2017Caper.html %}).

_posts/2017-02-01-Gian_viva.md

@@ -12,4 +12,4 @@ clients that interact with the API. The examiners found that Gian’s work conta
 on formal specification and verifications of concurrent software systems and recommended 
 that the viva is passed with only minor corrections. 
 
-More details on Gian’s research can be found [here](https://psvg.doc.ic.ac.uk/people/ntzik.html).
+More details on Gian’s research can be found [here]({{site.baseurl}}{% link _people/ntzik.md %}).