.gitlab-ci.yml

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

_people/gardner.md

@@ -32,4 +32,4 @@ 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', 2021](http://www.newton.ac.uk/event/vso). 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).
+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: Loow
+lastname: Lööw
 position: Researcher
-webpage: 
+webpage: https://www.doc.ic.ac.uk/~aloow/
 email: a.loow@imperial.ac.uk
-github: 
+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. Andreas defended his thesis, Building Verified Hardware and Verified Stacks in HOL, in September 2021.
+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/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.

_posts/2021-05-06-talk.md

+---
+title: Public Tech Talk on Gillian Verification of JavaScript and C, Galois
+---
+
+Philippa Gardner gave a public [live-stream](https://youtu.be/DqlC1tNElrg) technical talk on Gillian, Verification of JavaScript and C, hosted by [Galois](https://galois.com/about/). 
+
+The talk gave a general introduction to [Gillian](https://gillianplatform.github.io/), a platform for the development of symbolic-execution tools for many programming languages.
+
+Galois is a company specialising on applying [formal analysis techniques to the design of critical software systems](https://galois.com/research-development/). It runs a program of public [technical talks](https://galois.com/blog/category/tech-talks/), many of which are available online. 

_posts/2021-10-03-andreas.md

 ---
-title: Welcome to Andreas Loow, new researcher with the group
+title: Welcome to Andreas Lööw, new researcher with the group
 ---
 
-A very warm welcome to Andreas Loow, who has just started with us as a Post-Doctoral researcher. 
+A very warm welcome to Andreas Lööw, who has just started with us as a Post-Doctoral researcher. 
 
 Andreas completed his PhD on [Building Verified Hardware and Verified Stacks in HOL](https://www.doc.ic.ac.uk/~aloow/papers/thesis.pdf) at Chalmers University of Technology, under the supervision of [Magnus Myreen](http://www.cse.chalmers.se/~myreen/). 
 

_posts/2021-11-01-sacha_amazon.md

+---
+title: Sacha Ayoun, internship with Amazon Web Services
+---
+
+Welcome back to Sacha who has returned from a three-months internship with the CodeGuru team at Amazon Web Services.
+
+Amazon CodeGuru is a [set of publicly available developer tools](https://aws.amazon.com/codeguru/) that use machine learning to automatically review code for bugs and code quality and to suggest improvements.
+
+While at AWS, Sacha developed a proof of concepts analysis for Java that could help reduce the number of false positives or reduce the search space in other kinds of analyses without compromising soundness. Having enjoyed his time at AWS, he is planning to return for a second internship with them next year.

_posts/2021-11-05-his.md

+---
+title: Philippa Gardner, talk at High Integrity Software (HIS) conference
+---
+
+Philippa gave a talk on [Verified Trustworthy Software Specification](https://www.his-conference.co.uk/index.php?p=session/verified-trustworthy-software-systems) at this year's [High Integrity Software (HIS) Conference](https://www.his-conference.co.uk/).
+
+Now in its sixth year, [HIS](https://www.his-conference.co.uk/index.php?p=programme) aims to create a forum to share challenges, best practice and experience between software engineering practitioners. This year's HIS conference, under the theme: Assuring security and safety for critical software applications, focussed on cyber safety for embedded systems, innovations in testing and the application of formal methods to achieve cyber security.

_posts/2022-03-29-Gabi_viva.md

+---
+title: Congratulations to Dr Sampaio
+---
+
+Many congratulations to Gabriela Sampaio, who defended her PhD thesis, A Trusted Infrastructure for Symbolic Analysis of Event based Web APIS very succesfully today.
+
+Many thanks also to [Alan Schmitt](http://people.rennes.inria.fr/Alan.Schmitt/), [Frank Tip](http://www.franktip.org) and [Nicolas Wu](https://zenzike.com), who acted as the examiners.
+
+Gabriela's thesis presents her work developing a formal, executable semantics of a subset of the JavaScript programming language, including several key Application Program Interfaces (APIs) called [JaVerT.Click](https://github.com/javert-click/javert-click). The formalization models the Document Object Model (DOM) by which code executed in a browser interacts with the page that is being displayed, the JS promises and async/await mechanisms for asynchronous programming, and the WebMessaging and WebWorkers APIs for creating multiple workers that execute concurrently and communicate among each other using message-passing. The semantics can be instantiated to achieve either concrete or symbolic execution, enabling the construction of symbolic test cases that enable concise specification of tests that achieve good code coverage. 
+
+After a well deserved holiday, Gabriela will take up a position as a software engineer with Facebook London.

_posts/2022-04-04-rust.md

+---
+title: Talk at Rust Verification Workshop, ETAPS 2022
+---
+
+
+Sacha Ayoun and Petar Maksimovic gave a talk on Gillian-Rust: Unified Symbolic Analysis for Rust at the [Second Rust Verification Workshop (RW2022)](https://sites.google.com/view/rustverify2022/home), which was held in Munich, Germany, co-located with [ETAPS 2022](https://etaps.org/2022/)
+
+[Rust](https://www.rust-lang.org/) is a new programming language for writing performant code with strong type and memory safety guarantees, and a strong contender to becoming an alternative to C and C++ for systems programming. This has resulted in a growing interest in the program verification community for building program verifiers for Rust. 
+
+Following on from the first [Rust Verification Workshop in 2021](https://sites.google.com/view/rustverify2021/homes), this second workshop was aimed at language designers, application developers and formal verification tool builders, and intended as a forum for sharing research and build collaborations around developing verified Rust programs. Abstracts of the talks and slides will be avaible soon on the [Rust Verification Workshop](https://sites.google.com/view/rustverify2022/home). 

_posts/2022-04-26-daniele.md

+---
+title: Welcome to Daniele Nantes, new researcher with the group
+---
+
+A very warm welcome to Daniele Nantes Sobrinho, who has joined the group as a research assistant. Daniele is a tenured assistant professor at the [Department of Mathematics, University of Brasília](https://euro-math-soc.eu/affiliation/department-mathematics-university-brasilia), and is currently in a long sabbatical leave.
+
+Daniele’s research focusses on equational reasoning and comparative expressiveness of models and languages with concurrency. You can see her [latest publications here](http://vtss.doc.ic.ac.uk/people/nantes.html).

_posts/2022-05-15-floc22.md

+---
+title: Daniele Nantes, papers accepted at FSCD, FLoC 2022
+---
+
+Daniele Nantes has had two papers accepted at [FSCD, the 7th International Conference on Formal Structures for Computation and Deduction](https://www.cs.tau.ac.il/~nachumd/FSCD/), part of the [8th Federated Logic Conference (FLoC 2022)](https://www.floc2022.org/)
+
+Daniele will present the papers, [Nominal Anti-Unification with Atom Variables](https://drops.dagstuhl.de/opus/volltexte/2022/16288/), with Schmidt-Schauss and [A Certified Algorithm for AC Unification](https://drops.dagstuhl.de/opus/volltexte/2022/16289/), with Ayala-Rincón, Férnandez, and Ferreira da Silva, at this year’s conference, which will be held in Haifa, Israel.

_posts/2022-06-02-julian.md

+---
+title: Many congratulations to Dr Julian Sutherland
+---
+
+We are very, very happy to announce that Julian Sutherland, a long standing member of the group, has very successfully defended his PhD thesis today. 
+
+Many congratulations to Julian, and many thanks to [Derek Dreyer](https://www.mpg.de/18617632/software-systems-dreyer), [Joseph Tassarotti](http://www.cs.bc.edu/~tassarot/) and [Sophia Drossopoulou](https://wp.doc.ic.ac.uk/sd/), who acted as the examiners.
+
+Julian’s thesis, Compositional termination verification for fine-grained concurrency, focuses on TaDA Live, a separation logic for proving liveness properties of concurrent programs.  
+
+Liveness properties are concerned with showing that a program eventually reaches some desired state, in contrast to safety properties, which involve showing that a program never reaches a "bad/unsafe" state. Research work on proving liveness properties remains challenging and TaDA Live represents a substantial innovation, as it can handle reasoning about both non-blocking and blocking examples. 
+
+TaDA Live can reason about the termination of clients which use abstract atomic operations that have blocking behaviour arising from busy-waiting patterns without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. The thesis also introduces a novel semantic model using layered subjective obligations to express liveness invariants, and a proof system that is sound with respect to the model.
+
+Julian is currently a Formal Verification Engineer at [Nethermind](https://nethermind.io/), a blockchain company working on Ethereum.