Commit 25bd984c authored by pmaksimo's avatar pmaksimo

gillian

parent 3e49278b
Pipeline #142075 passed with stages
in 5 minutes and 53 seconds
......@@ -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>
......
......@@ -7,15 +7,15 @@ email: s.ayoun17@imperial.ac.uk
github: https://github.com/Giltho/
alumnus: false
projects:
- web
- gillian
- moc
---
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
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
......@@ -10,8 +10,9 @@ 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
......@@ -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
Fellowship at Imperial, 2005-2009.
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
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
......@@ -11,8 +11,9 @@ 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ć 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/).
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
Subproject commit 407bb7cd107cb8a9ef7148b4bb51b98bb17a6080
Subproject commit 2b4da9020b01c42f46387f90ad6a4a18333d15c5
---
title: Gillian
project_id: gillian
menu: true
parent_menu: Research
menu_order: 4
sub_menu_order: 2
---
Gillian is a multi-language platform for the development
of compositional symbolic analysis tools. Gillian currently
supports three flavours of analysis: whole-program symbolic
testing, full verification based on separation logic, and
automatic compositional testing based on bi-abduction.
These analysis are, for the first time, unified in a
common symbolic execution engine.
#### GIL
At the core of Gillian is GIL, a simple goto intermediate
language that is parametric on the basic actions of the
memory model of the target language (TL); that is, the ways
in which TL-programs fundamentally interact
with their memories.
#### Correctness
The symbolic execution of Gillian is fully formalised, with
the implementation closely following the formalisation.
The correctness results are, for the first time, stated
and proven parametrically, independently of the TL.
This has been made possible by a novel concept of restriction,
which generalises path conditions of classical symbolic execution.
#### Instantiations
In order to instantiate Gillian to a new target language,
the tool developer has to provide:
- a trusted, memory-preserving compiler from the TL to GIL instantiated with the TL basic actions;
- an OCaml implementation of the concrete and symbolic memory models of the TL; and
- for the meta-theory, proofs for only two lemmas on the TL basic actions.
So far, we have instantiated Gillian to JavaScript and C.
#### Publications
We have recently published the first paper on Gillian at PLDI'20 (see below), which
introduces the principles of Gillian, its core symbolic execution, and its symbolic testing.
\ No newline at end of file
---
title: JavaScript
title: Web Programs
project_id: web
menu: true
parent_menu: Research
menu_order: 4
sub_menu_order: 2
sub_menu_order: 3
---
We study the mechanised specification of the JavaScript language
......@@ -31,7 +31,7 @@ We have developed a principled compiler from JavaScript (ECMAScript 5
strict) to a small intermediate language JSIL, which has a simpler
operational semantics and is better suited to program verification.
The compiler has been substantially tested using the Test262 test
suite and it comes with a hand-proof of translation correctness
suite and it comes with a hand-proof of translation correctness
for a fragment of the language. We will use JSIL to develop JSVerify - a
verification tool for JavaScript. Daiva Naudžiūnienė will
this year hold internships at Amazon and Facebook to use
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment