_includes/person-cards-small.html

+<div class="people">
+{% for person in include.people %}{% assign row = forloop.index | modulo: include.people.size %}
+{% if row == 1%}<div class="card-deck-wrapper"><div class="card-deck">{% endif %}
+<div class="card p-0">
+  <div class="card-block text-xs-center people">
+    <a href="{{ person.url }}">
+      {% include person-photo-small.html %}
+      <h6 class="card-title small-title">{{ person.firstname }}<br/>{{ person.lastname }}</h6>
+    </a>
+  </div>
+</div>
+{% if row == 0 or forloop.last %}</div></div>{% endif %}
+{% endfor %}
+</div>

_includes/person-cards.html

 <div class="people">
-{% for person in include.people %}{% assign row = forloop.index | modulo: 3 %}
+{% for person in include.people %}{% assign row = forloop.index | modulo: 4 %}
 {% if row == 1%}<div class="card-deck-wrapper"><div class="card-deck">{% endif %}
 <div class="card">
   <div class="card-block text-xs-center people">
     <a href="{{ person.url }}">
       {% include person-photo.html %}
-      <h4 class="card-title">{{ person.firstname }} {{ person.lastname }}</h4>
+      <h6 class="card-title" style="font-weight:bold">{{ person.firstname }} {{ person.lastname }}</h6>
     </a>
     <h6 class="card-subtitle text-muted">{{ person.position }}</h6>
   </div>
 </div>
-{% if row == 0%}</div></div>{% endif %}
+{% if row == 0 or forloop.last %}</div></div>{% endif %}
 {% endfor %}
 </div>

_includes/person-photo-small.html

+{% assign path = person.url | prepend: '/images' | replace: '.html','.jpg' %}
+{% assign file = site.static_files | where: "path", path | first %}
+{% if file %}
+<img class="person-img-small img-circle" src="{{ file.path }}" alt="Photo of {{ person.firstname }} {{ person.lastname }}" />
+{% else %}
+<div class="person-img-small fa-stack fa-5x"><i class="fa fa-circle fa-stack-2x"></i><i class="fa fa-user fa-stack-1x fa-inverse"></i></div>
+{% endif %}

_includes/publication-authors.html

 <ul class="list-inline">
 {% for author in include.authors %}
-{% assign matched = site.people | where:"lastname",author.last | first %}
+{% assign matched = site.people | where:"lastname", author.last | first %}
+{% unless matched %}{% assign slug = author.last | slugify %}{% assign matched = site.people | where:"slug", slug | first %}{% endunless %}
 <li class="list-inline-item">{% if matched %}<a href="{{ matched.url }}">{% endif %}{{ author.first }} {{ author.last }}{% if matched %}</a>{% endif %}</li>
 {% endfor %}
 </ul>

_includes/publication-venue.html

-{% if include.entry.jorurnal %}{{ include.entry.journal }}{% elsif include.entry.booktitle %}{{ include.entry.booktitle }}{% elsif include.entry.institution %}{{ include.entry.institution }}{% elsif include.entry.school %}{{ include.entry.school }}{% endif %}
+{% if include.entry.journal %}
+	{{ include.entry.journal }}, 
+	vol. {{ include.entry.volume }}{% if include.entry.number %}({{ include.entry.number }}){% endif %}{% if include.entry.pages %}, pp. {{ include.entry.pages }}{% endif %}
+	{% elsif include.entry.booktitle %}
+		{{ include.entry.booktitle }}{% if include.entry.pages %}, pp. {{ include.entry.pages }}{% endif %}
+			{% elsif include.entry.school %}
+				{% if include.entry.phdthesis %}Ph.D. Thesis, {% endif %}{{ include.entry.school }}
+{% endif %}
\ No newline at end of file

_layouts/home.html

@@ -5,23 +5,21 @@ layout: default
   <div class="lead">
     {{ content }}
   </div>
-  <a class="btn btn-primary btn-lg" href="{{ site.pages | where:'title','Research' | map:'url' }}">Our Research</a>
+  {% assign research_pages = site.pages | where_exp: 'page', 'page.url contains "/research/"'%}
+  {% for item in research_pages %}
+  <a class="btn btn-primary btn-lg" href="{{ item.url }}">{{ item.title }}</a>
+  {% endfor %}
 </div>
 
 
 <div class="row">
   <div class="col-sm-6">
-    <h2>News</h2>
-      {% for post in site.posts %}
-      <h3 class="blog-post-title"><a href="{{ post.url }}">{{ post.title }}</a></h3>
-      <p class="blog-post-meta">{{ post.date | date: "%b %-d, %Y" }}</p>
-      {{ post.excerpt}}
-      {% endfor %}
-    </div>
+    <h2><a href="{% link news.html %}">Recent News</a></h2>
+    {% include news-page.html max=5 %}
+  </div>
 
   <div class="col-sm-6">
-    <h2>Recent Publications</h2>
+    <h2><a href="{% link publications.html %}">Recent Publications</a></h2>
     {% bibliography --max 5 %}
   </div>
 </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 %}

_layouts/post.html

@@ -12,4 +12,11 @@ layout: default
     {{ content }}
   </div>
 
+  <nav>
+    <ul class="pager">
+      {% if page.previous %}<li><a href="{{ page.previous.url }}">Previous</a></li>{% endif %}
+      {% if page.next %}<li><a href="{{ page.next.url }}">Next</a></li>{% endif %}
+    </ul>
+  </nav>
+
 </article>

_layouts/publication-entry.html

@@ -3,6 +3,5 @@
   {% if link %}<a class="btn btn-secondary" role="button" href="{{ link }}"><i class="fa fa-file-text-o"></i></a>{% endif %}
 </div>
 <p class="pub-title h4"><a href="{{ details }}">{{ entry.title }}</a></p>
-<p class="pub-authors">{% include publication-authors.html authors=entry.author_array %}</p>
+{% include publication-authors.html authors=entry.author_array %}
 <p class="pub-venue">{% include publication-venue.html entry=entry %}</p>
-

_layouts/publication.html

 ---
 layout: page
 menu: false
+
+# The display of the Source Materials Section can be configured in _data/publication_file_types.yml
 ---
 <div class="row">
   <div class="col-sm-4">
@@ -22,7 +24,7 @@ menu: false
   </div>
   <div class="col-sm-8">
     <h3>Authors</h3>
-    <p>{% include publication-authors.html authors=page.entry.author_array %}</p>
+    {% include publication-authors.html authors=page.entry.author_array %}
 
     {% if page.entry.abstract %}
     <h3>Abstract</h3>
@@ -31,29 +33,33 @@ menu: false
     </p>
     {% endif %}
 
-    <h3>Full Text</h3>
-    {% if page.entry.numpages %}<p>{{ page.entry.numpages }} pages</p>{% endif %}
-    {% if page.entry.doi or page.link %}
+    {% if page.entry.doi or page.links.size > 0 %}
+    <h3>Source Materials</h3>
     <ul class="fa-ul">
-      {% if page.link %}<li><a href="{{ page.link }}"><i class="fa fa-li fa-file-text-o"></i>Authors' Preprint</a></li>{% endif %}
-      {% if page.entry.doi %}<li><a href="http://dx.doi.org/{{ page.entry.doi }}"><i class="fa fa-li
-      fa-external-link"></i>Published Edition</a></li>{% endif %}
-    </ul>
-    {% else %}
-    <p>Available on request</p>
-    {% endif %}
+      {% comment %} Iterate all known types in the defined order {% endcomment %}
+      {% assign types = site.data.publication_file_types %}
+      {% for type in types %}
+      {% if page.links[type.ext] %}
+      {% capture link %}{% if type.include %}{% assign file = page.links[type.ext] | split: "/" | last %}{% include_relative {{file}} %}{% else %}{{ page.links[type.ext] }}{% endif %}{% endcapture %}
+      <li><a href="{{ link }}"> <i class="fa fa-li {{ type.icon }}"></i>{{ type.text }} </a></li>
+      {% endif %}
+      {% endfor %}
 
-    {% comment %}
-    <h3>Supplementary Material</h3>
-    <ul class="fa-ul">
-      <li><a href=""><i class="fa fa-li fa-file-text-o"></i>Technical Report</a></li>
-      <li><a href=""><i class="fa fa-li fa-file-archive-o"></i>Download (.zip)</a></li>
-      <li><a href=""><i class="fa fa-li fa-code-fork"></i>Code Repository</a></li>
-      <li><a href=""><i class="fa fa-li fa-file-code-o"></i>Code File</a></li>
-    </ul>
-    {% endcomment %}
+      {% comment %} Iterate all files and pick unknown file types {% endcomment %}
+      {% assign known_types = types | map: "ext" %}
+      {% for link in page.links %}
+      {% unless known_types contains link[0] %}
+      <li><a href="{{ link[1] }}"><i class="fa fa-li fa-file-o"></i>
+          {{ link[0] }} File</a></li>
+      {% endunless %}
+      {% endfor %}
+
+      {% if page.entry.doi %}<li><a href="http://dx.doi.org/{{ page.entry.doi }}"><i class="fa fa-li fa-external-link"></i>
+          Published Edition</a></li>{% endif %}
 
-    <h3>Export Citation</h3>
-    <textarea class="form-control" rows="10">{{ page.entry.bibtex }}</textarea>
+      <li><a download="{{page.entry.key}}.bib" href="data:application/x-bibtex,{{ page.entry.bibtex | uri_escape }}">
+          <i class="fa fa-li fa-at"></i>BibTeX Citation</a></li>
+    </ul>
+    {% endif %}
   </div>
 </div>

_layouts/research.html

@@ -6,9 +6,9 @@ layout: page
 {% assign people = site.people | where_exp: "person", "person.projects contains page.project_id" %}
 {% if people.size > 0 %}
 <h3>People</h3>
-{% include person-cards.html people=people %}
+{% include person-cards-small.html people=people %}
 {% endif %}
 
 <h3>Recent Publications</h3>
 
-{% bibliography -q @*[project ~= {{page.project_id}}] --max 5 %}
+{% bibliography -q @*[project ~= {{page.project_id}}] --max 10 %}

_layouts/teaching.html

+---
+layout: page
+---
+{{ content }}
+
+{% assign people = site.people | where_exp: "person", "person.projects contains page.project_id" %}
+{% if people.size > 0 %}
+<h3>People</h3>
+{% include person-cards-small.html people=people %}
+{% endif %}

_people/ayoun.md

+---
+firstname: Sacha
+lastname: Ayoun
+position: PhD Student
+webpage: https://www.doc.ic.ac.uk/~sja3417/
+email: s.ayoun17@imperial.ac.uk
+github:  https://github.com/Giltho/
+alumnus: false
+projects:
+  - gillian
+  - sl
+---
+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: Researcher
+webpage: https://mbodin.github.io/index.html?lang=en&pedanticJS=no#en
+email: mbodin@ic.ac.uk
+github:
+alumnus: true
+projects:
+  - web
+---
+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: Researcher
+github: acerone85
+alumnus: true
+projects:
+  - concurrency
+  - moc
+---
+
+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: Researcher
+webpage: http://www.emanueledosualdo.com/
+email: e.dosualdo@imperial.ac.uk
+github: bordaigorl
+alumnus: true
+projects:
+  - concurrency
+---
+
+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

@@ -5,8 +5,9 @@ position: PhD Student
 webpage: http://www.doc.ic.ac.uk/~pmd09/
 email: pmd09@doc.ic.ac.uk
 github: pedromdrp
-projects:
-  - concurrency
+alumnus: true
 ---
-Pedro da Rocha Pinto is a PhD student at the [Department of Computing](http://www.doc.ic.ac.uk) at
-Imperial. His research focusses on developing logics for verification of fine-grained concurrent programs.
+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: true
 projects:
-  - javascript
+  - 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

@@ -4,19 +4,32 @@ lastname: Gardner
 position: Professor, Group Leader
 webpage: http://www.doc.ic.ac.uk/~pg/
 email: pg@doc.ic.ac.uk
+alumnus: false
 projects:
+  - web
   - concurrency
+  - sl
+  - moc
+  - infer
+  - gillian
 ---
-Philippa Gardner is a professor in the [Department of Computing](http://www.doc.ic.ac.uk) at
-Imperial. 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 is the
- Director of the [Research Institute in Automated Program Analysis and Verification](http://www.verificationinstitute.org),
-funded by GCHQ in association  with EPSRC.
+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', 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.