Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • verified-software/psvg.doc.ic.ac.uk
  • xr119/psvg.doc.ic.ac.uk
2 results
Show changes
Hide whitespace changes
Inline Side-by-side
publications @ 2b4da902
Subproject commit 407bb7cd107cb8a9ef7148b4bb51b98bb17a6080
Subproject commit 2b4da9020b01c42f46387f90ad6a4a18333d15c5
research/concurrency.md
View file @ f3f745d5
......@@ -7,13 +7,8 @@ menu_order: 4
sub_menu_order: 1
---
We develop formal reasoning techniques for concurrent programs, with a
particular emphasis on concurrent program logics. Recently, various
logics based on separation logic have been developed, by ourselves and
others, to provide more modular abstract reasoning about concurrent programs.
Our work has tackled a range of problems including data abstraction,
abstract atomicity, fault-tolerance and progress. In particular, we
have recently developed {% cite_details Dinsdale-Young2010Concurrent --text Concurrent Abstract Predicates %}, {% cite_details Dinsdale-Young2013Views --text Views %}, {% cite_details daRochaPinto2014TaDA --text TaDA %}, {% cite_details Raad2015CoLoSL --text CoLoSL %}, {% cite_details Ntzik2015Fault --text Fault-tolerant Concurrent Separation Logic %} and {% cite_details daRochaPinto2016Modular --text Total-TaDA %}.
We develop compositional reasoning techniques for concurrent programs using modern concurrent separation logics, introducing
fundamental concepts in the reasoning: logical abstraction [(Concurrent Abstract Predicates)], logical atomicity [(the TaDA Logic)] and logical environment liveness properties [(TaDA Live)]. In addition, we have started to work on weak consistency models for distribution, developing an interleaving operational semantics for client-observational behaviour of atomic transactions [(ECOOP’20)].
We have applied our reasoning to, for example, algorithms for
manipulating concurrent B-trees, skip lists from
......@@ -25,15 +20,21 @@ logics, and applying our work to real-world concurrent programs.
#### Research Support
This research is supported by the EPSRC programme grant
This research is supported by Gardner's UKRI Established Career Fellowship
["VeTSpec: Verified Trustworthy Software Specification"][VeTSpec] and
Emanuele D'Osualdo's Marie-Curie Fellowship "VeSPA: Verification through
Security and Progress Abstractions".
It was previously supported by the EPSRC programme grant
[EP/K008528/1]: [REMS: Rigorous Engineering of Mainstream
Systems][REMS] and previously by the EPSRC programme grant [EP/H008373/2]: [Resource
Reasoning]. We also have substantial collaboration with [Thomas Dinsdale-Young],
previously a PhD student and RA of Gardner and now an independent
research fellow at the University of Aarhus.
Systems][REMS] and the EPSRC programme grant [EP/H008373/2]: [Resource
Reasoning].
[VeTSpec]: https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/R034567/1
[EP/K008528/1]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K008528/1
[REMS]: http://www.cl.cam.ac.uk/~pes20/rems/
[EP/H008373/2]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/H008373/2
[Resource Reasoning]: http://www.resourcereasoning.com/
[Thomas Dinsdale-Young]: http://cs.au.dk/~tyoung/
[(Concurrent Abstract Predicates)]: https://vtss.doc.ic.ac.uk/publications/Dinsdale-Young2010Concurrent.html
[(the TaDA Logic)]: https://vtss.doc.ic.ac.uk/publications/daRochaPinto2014TaDA.html
[(TaDA Live)]: https://vtss.doc.ic.ac.uk/publications/DOsualdo2020TaDA.html
[(ECOOP’20)]: https://vtss.doc.ic.ac.uk/publications/Xiong2020Data.html
research/gillian.md 0 → 100644
View file @ f3f745d5
---
title: Gillian
project_id: gillian
menu: true
parent_menu: Research
menu_order: 4
sub_menu_order: 2
---
[Gillian](https://gillianplatform.github.io/) is a multi-language platform for the development
of compositional symbolic analysis tools. Gillian currently
supports three flavours of analysis: 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 memory model of the target language (TL):
that is, on the set of basic actions capturing 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 classic symbolic execution.
#### Instantiations
In order to instantiate Gillian to a new TL,
the tool developer has to provide:
- a trusted compiler from the TL to GIL instantiated with the TL basic actions, preserving the TL memory model and semantics;
- an OCaml implementation of the concrete and symbolic memory models of the TL; and
- for the meta-theory, proofs of simple lemmas for 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.
#### Research Support
Gillian is supported by Gardner's UKRI Established Career Fellowship
["VeTSpec: Verified Trustworthy Software Specification"][VeTSpec], Facebook,
and GCHQ. It was previously supported by the EPSRC programme grant
[EP/K008528/1]: [REMS: Rigorous Engineering of Mainstream Systems][REMS].
[VeTSpec]: https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/R034567/1
[EP/K008528/1]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K008528/1
[REMS]: http://www.cl.cam.ac.uk/~pes20/rems/
research/javascript.md
View file @ f3f745d5
---
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
(following the ECMAScript 5 standard) and the verification of
JavaScript programs.
We study the testing and verification of JavaScript programs and Web APIs, and mechanised language specification using JavaScript as the real-world example language.
#### JSCert
#### JaVerT
We have developed [JaVerT], a compositional symbolic analysis tool for JavaScript, targeting the strict mode of the ECMAScript 5 standard. JaVerT supports whole-program symbolic testing, verification and automatic compositional testing based on bi-abduction. It comprises:
- JSIL, an intermediate goto language with a symbolic execution engine with explicit management of execution errors that guides the feedback for symbolic testing and the automatic bi-abductive inference. The meta-theory underpinning JSIL is formally defined and modular, streamlining the proofs and guiding the implementation.
- JS-2-JSIL, a trusted compiler that preserves the JavaScript memory model and semantics, trusted in the sense that it is line-by-line close to the standard and comprehensively tested using the official Test262 test suite.
#### Web APIs
Using our considerable experience with the DOM specification and JavaScript analysis, we have recently [(ECOOP'20)] introduced a trusted infrastructure for symbolic analysis of modern event-driven Web applications, comprising:
- reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises, and the JavaScript async/await APIs, all following the API standards as closely as possible and all thoroughly tested against the official test suites;
- a simple Core Events Semantics that is sufficiently expressive to describe the event models underlying these APIs;
- JaVerT.Click, an extension of JaVerT with the Core Events Semantics, that is, for the first time, able to symbolically test JavaScript programs that use any/all of the above-mentioned APIs.
We have used JaVerT.Click to analyse the events module of [cash](https://kenwheeler.github.io/cash/), a small, widely-used jQuery alternative, in which we found two bugs (fixed) and for which we have proven boundned correctness of several essential properties, such as "an event handler can be triggered if and only if it has previously been registered".
We have also found a bug in the [p-map](https://github.com/sindresorhus/p-map) library (fixed), which extends the functionality of JavaScript Promises.
#### Language Semantics
With Bodin, Charguéraud, and Schmitt at Inria, we
have developed [JSCert](http://jscert.org/), a substantial Coq specification that is
line-by-line close to the core language of the ECMAScript 5
standard. It comes with a reference interpreter, JSRef, proven correct
with respect to JSCert and tested using the official Test262 test
suite. We are currently extending this specification to the
numerous libraries, providing continuous test integration for the
ever-growing specification, developing a new, human-readable JSRef,
with a tighter connection to the standard and good tracking
properties, and creating the web service Explain.js to explain
behavioural complexities of JavaScript programs.
#### JSIL
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
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
JSIL to develop front-ends for the CBMC and Infer verification tools.
suite. With Schmitt and Jensen, we have also recently introduced the skeletal semantics framework
for capturing both concrete and abstract semantics, connected together by a
general consistency result. Our hope is that this framework will simplify
the verification of properties such has heap well-formedness for large
complex languages such as JavaScript.
#### Research Support
This research is supported by the EPSRC
This work is supported by Gardner's UKRI Established Career Fellowship
["VeTSpec: Verified Trustworthy Software Specification"][VeTSpec].
It was previously supported by the EPSRC
programme grant [EP/K008528/1]: [REMS: Rigorous Engineering of
Mainstream Systems][REMS] and previously by the EPSRC/GCHQ grant [EP/K032089/1]:
[Certified Verification of Client-Side Web Programs][1] and the EPSRC
programme grant [EP/H008373/2]: [Resource Reasoning].
We also interact extensively with [Arthur Charguéraud], [Alan Schmitt] and
[Martin Bodin] of INRIA, who are supported by the [AJACS] project.
Mainstream Systems][REMS], the EPSRC/GCHQ grant [EP/K032089/1]:
[Certified Verification of Client-Side Web Programs][1], and the EPSRC
programme grant [EP/H008373/2]: [Resource Reasoning]. We also have
substantial collaboration with [José Fragoso Santos], previously an RA
in the group and now an Assistant Professor at the Instituto
Superior Técnico, Lisbon.
[VeTSpec]: https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/R034567/1
[EP/K032089/1]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K032089/1
[EP/H008373/2]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/H008373/2
[EP/K008528/1]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K008528/1
......@@ -56,5 +62,7 @@ We also interact extensively with [Arthur Charguéraud], [Alan Schmitt] and
[Resource Reasoning]: http://www.resourcereasoning.com/
[Arthur Charguéraud]: http://www.chargueraud.org/
[Alan Schmitt]: https://www.irisa.fr/celtique/aschmitt/
[Martin Bodin]: http://people.irisa.fr/Martin.Bodin/index.html?lang=en
[José Fragoso Santos]: http://web.ist.utl.pt/jose.fragoso/
[AJACS]: http://ajacs.inria.fr/
[JaVerT]: https://vtss.doc.ic.ac.uk/publications/FragosoSantos2019JaVerT.html
[(ECOOP'20)]: https://vtss.doc.ic.ac.uk/publications/Sampaio2020Trusted.html
teaching/ModelsComputation.md
View file @ f3f745d5
......@@ -15,17 +15,15 @@ The course focuses on teaching students the fundamental skills involved in deali
This course provides a whirlwind tour of some of the key concepts in theoretical computer science.
In particular, we will study formal descriptions (models) of computational behaviour.
#### General Information for 2019 autumn term
#### General Information for 2021 autumn term
Time: Wednesdays: 9am - 11am, Room 311.
Thursdays: 12 - 1pm, Room 311.
Time: Mondays: 11am - 12am, Room TBC and Fridays: 4pm - 6pm, Room TBC.
Coursework Schedule:
Assesed coursework 1: published Weds 30th Oct, 9 AM / deadline for submission Fri 8th Nov, 4 PM.
Assesed coursework 1: published TBC / deadline for submission TBC.
Assesed coursework 2: published Wed 27th Nov, 9 AM / deadline for submission Tue 10th Dec, 4 PM.
Assesed coursework 2: TBC / deadline for submission TBC.
Tutorials: Tutorial exercises will be posted online (here and on CATE) before the tutorial each week, printed copies will also be available.
Tutorial solutions will be published online before the next week's tutorial.
......
teaching/separationlogic.md
View file @ f3f745d5
---
title: Separation Logic
title: Scalable Software Verification
project_id: sl
menu: false
parent_menu: Teaching
......@@ -7,12 +7,11 @@ menu_order: 5
sub_menu_order: 1
---
The Separation Logic course is a 4th year MEng and MSc course on local reasoning about programs that manipulate the heap at the [Department of Computing](http://www.imperial.ac.uk/computing), [Imperial College London](http://www.imperial.ac.uk).
The Scalable Software Verification course (formerly Separation Logic)is a 4th year MEng and MSc course on local reasoning about programs that manipulate the heap at the [Department of Computing](http://www.imperial.ac.uk/computing), [Imperial College London](http://www.imperial.ac.uk).
#### Description of the Course
In the late 1960s, Tony Hoare developed Hoare logic, a formal system with a set of rules for reasoning rigorously about the correctness of imperative programs that alter the variable state. However, Hoare logic is not good at reasoning about imperative programs that alter the heap state, since the reasoning does not scale.
In 2001, building on Hoare's work and early ideas from Burstall, O'Hearn and Reynolds introduced separation logic, in which the reasoning does scale.
In the late 1960s, Tony Hoare developed Hoare logic, a formal system with a set of rules for reasoning rigorously about the correctness of imperative programs that alter the variable state. However, Hoare logic is not good at reasoning about imperative programs that alter the heap state, since the reasoning does not scale. In 2001, building on Hoare's work and early ideas from Burstall, O'Hearn and Reynolds introduced separation logic, in which the reasoning does scale.
This course will provide a whirl-wind tour of separation logic, its verification tools and cutting-edge research on reasoning about concurrent programs.
Separation logic was introduced to reason about shared mutable data structures represented in the heap: in particular, to catch memory overruns and null-pointer dereferencing.
......@@ -35,11 +34,11 @@ This work constitutes a breakthrough, in that it is now possible prove propertie
* The last week will provide an introduction to concurrent separation logics. With Brookes, O'Hearn won the Godel prize for this work in 2016.
#### General Information for 2019 autumn term
#### General Information for 2021 autumn term
*Time:* Tuesdays 2pm-4pm, 2nd through 9th week, Room 130.
*Time:* Mondays 2pm-4pm, 2nd through 9th week, Room 145 and Thursdays 11am-1pm, 2nd through 9th week, Room 145
*Coursework:* Published Tues 29th Oct, 9 AM / deadline Fri 8th Nov, 4 PM.
*Coursework:* Published TBC / deadline TBC.
*Exam:* The exam will take place December, date and time TBC. It will last for 70 minutes.
You will be given three questions, out of which you need to answer two of your choice.
......@@ -75,18 +74,17 @@ da Rocha Pinto, Dinsdale-Young, Gardner, MFPS 2015, describes some modern develo
There are many additional interesting links given on the [Piazza](https://piazza.com) site and below.
If you have further suggestions on what reading material might be of interest, please let us know.
Public lecture by Tony Hoare entitled ["Could computers understand their own programs?"](http://www.cambridgephilosophicalsociety.org/) on Nov. 19 at 6pm
Public lecture by Tony Hoare entitled ["Could computers understand their own programs?"](https://www.cl.cam.ac.uk/seminars/wheeler/tony-hoare/), part of the annual Wheeler lectures series.
Alan Turing describes [his work on soundness, completeness, Gödel's theorem, Turing machines etc.](http://www.youtube.com/watch?v=S23yie-779k&t=28m26s)
A re recording of a broadcast by Alan Turing, describing [his work on soundness, completeness, Gödel's theorem, Turing machines etc.](hhttps://aperiodical.com/2018/01/ive-re-recorded-alan-turings-can-computers-think-radio-broadcasts/)
Floyd's [obituary](http://web.stanford.edu/dept/news/pr/01/floydobit117.html)
Floyd's [obituary](https://cs.stanford.edu/memoriam/professor-robert-w-floyd)
and his seminal 1967 paper [Assigning meanings to programs](http://www.cs.berkeley.edu/~necula/Papers/FloydMeaning.pdf)
Wikipedia article on [Hoare](http://en.wikipedia.org/wiki/Tony_Hoare)
and his seminal 1969 paper [An axiomatic basis for computer programming](http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf)
[Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems](http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/79_impossible_hoareaxiom.pdf) by Edmund M. Clarke Jr.
(http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/79_impossible_hoareaxiom.pdf)
[Zune bug](http://techcrunch.com/2008/12/31/zune-bug-explained-in-detail/) explained in detail
......@@ -94,8 +92,8 @@ and his seminal 1969 paper [An axiomatic basis for computer programming](http://
Microsoft projects:
[SLAM](http://research.microsoft.com/en-us/projects/slam/)
[T2 termination prover](http://research.microsoft.com/en-us/projects/t2/)
[SLAyer](http://research.microsoft.com/en-us/projects/t2/)
[T2 termination prover](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/04/t2-tool-report.pdf)
[SLAyer](https://www.microsoft.com/en-us/research/publication/slayer-memory-safety-for-systems-level-code/)
Wikipedia article on [Material Implication](http://en.wikipedia.org/wiki/Material_conditional)
the [Paradoxes of Material Implication](http://legacy.earlham.edu/~peters/courses/log/mat-imp.htm)
......@@ -105,7 +103,7 @@ Collection of [Software Bugs and Software Glitches](http://www5.in.tum.de/~huckl
The VCC verifier can be downloaded from http://vcc.codeplex.com or tried at http://www.rise4fun.com/vcc
Peter Homeier's [Sunrise system](http://www.cis.upenn.edu/~hol/sunrise/)
Peter Homeier's [Sunrise system](http://www.trustworthytools.com/id13.html)
[Design by Contract](http://www.eecs.ucf.edu/~leavens/JML/jmldbc.pdf) (a paper by Gary T. Leavens and Yoonsik Cheon)