From 3876da61e7d2a22ac12ef818fcdf5d2f8b8b1237 Mon Sep 17 00:00:00 2001
From: Shale XIONG <shalexiong@dyn1171-29.wlan.ic.ac.uk>
Date: Mon, 14 Nov 2016 11:19:29 +0000
Subject: [PATCH] Add separation course to the website.
---
_layouts/research.html | 2 ++
_people/da-rocha-pinto.md | 1 +
_people/fragoso-santos.md | 1 +
_people/gardner.md | 1 +
_people/naudziuniene.md | 1 +
_people/raad.md | 1 +
_people/sutherland.md | 1 +
research/Separation_Logic | 32 ---------------------
research/separationlogic.md | 57 +++++++++++++++++++++++++++++++++++++
9 files changed, 65 insertions(+), 32 deletions(-)
delete mode 100644 research/Separation_Logic
create mode 100644 research/separationlogic.md
diff --git a/_layouts/research.html b/_layouts/research.html
index 298dcb0..32e4cff 100644
--- a/_layouts/research.html
+++ b/_layouts/research.html
@@ -9,6 +9,8 @@ layout: page
{% include person-cards.html people=people %}
{% endif %}
+{% if page.project_id != "sl" %}
<h3>Recent Publications</h3>
{% bibliography -q @*[project ~= {{page.project_id}}] --max 10 %}
+{% endif %}
diff --git a/_people/da-rocha-pinto.md b/_people/da-rocha-pinto.md
index f33e03c..a5ddc68 100644
--- a/_people/da-rocha-pinto.md
+++ b/_people/da-rocha-pinto.md
@@ -7,6 +7,7 @@ email: pmd09@doc.ic.ac.uk
github: pedromdrp
projects:
- concurrency
+ - sl
---
Pedro da Rocha Pinto is a PhD student at the [Department of Computing](http://www.doc.ic.ac.uk) at
Imperial. His research focuses on developing logics for verification of fine-grained concurrent programs.
diff --git a/_people/fragoso-santos.md b/_people/fragoso-santos.md
index 1f915eb..ad2ddcc 100644
--- a/_people/fragoso-santos.md
+++ b/_people/fragoso-santos.md
@@ -7,4 +7,5 @@ email: jose.fragoso.santos@imperial.ac.uk
github: j3fsantos
projects:
- web
+ - sl
---
diff --git a/_people/gardner.md b/_people/gardner.md
index 46660ff..4fd869f 100644
--- a/_people/gardner.md
+++ b/_people/gardner.md
@@ -7,6 +7,7 @@ email: pg@doc.ic.ac.uk
projects:
- web
- concurrency
+ - sl
---
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.
diff --git a/_people/naudziuniene.md b/_people/naudziuniene.md
index 8e63577..c71d00c 100644
--- a/_people/naudziuniene.md
+++ b/_people/naudziuniene.md
@@ -6,4 +6,5 @@ webpage: http://www.doc.ic.ac.uk/~dn911/
email: d.naudziuniene11@imperial.ac.uk
projects:
- web
+ - sl
---
diff --git a/_people/raad.md b/_people/raad.md
index ad08f42..ac450e9 100644
--- a/_people/raad.md
+++ b/_people/raad.md
@@ -6,5 +6,6 @@ webpage: http://www.doc.ic.ac.uk/~azalea/
email: azalea@imperial.ac.uk
projects:
- concurrency
+ - sl
---
diff --git a/_people/sutherland.md b/_people/sutherland.md
index 2ea5a16..351c79f 100644
--- a/_people/sutherland.md
+++ b/_people/sutherland.md
@@ -6,5 +6,6 @@ webpage: http://www.doc.ic.ac.uk/~jhs110/
email: jhs110@doc.ic.ac.uk
projects:
- concurrency
+ - sl
---
diff --git a/research/Separation_Logic b/research/Separation_Logic
deleted file mode 100644
index 283e184..0000000
--- a/research/Separation_Logic
+++ /dev/null
@@ -1,32 +0,0 @@
----
-title: Separation_Logic
-menu: true
-menu_order: 4
----
-Separation Logic:Local Reasoning about Programs (404H)
-
-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. 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. It has been used to reason about C, Java and JavaScript programs, and algorithms for shared-memory concurrency. There are many academic verification tools, such as Smallfoot, Verifast and Abductor, and the industrial tool Infer (see http://fbinfer.com/), developed by a team led by Peter O'Hearn at Facebook. As well as Facebook, Infer is used by Instagram, kiuwan, oculus, Spotify, UBER, WhatsApp, Marks and Spencer, and Sky.
-
-Course Outline
-
-The course comprises two hours a week for seven weeks. It will be accompanied by comprehensive course notes, which bring together a variety of ideas from the most influential research papers.
-
-The first four weeks will provide a basic introduction to separation logic for reasoning about mutable data structures, using linked lists and binary trees as the primary examples. You will learn how to write program specifications and prove properties of programs, both informally using sketch proofs and formally using rigorous proofs. The next two weeks will describe tools, demonstrating that reasoning about real-world programs using separation logic is feasible. You will learn about Smallfoot, a semi-automatic verification tool based on symbolic execution, and Infer, an automatic tool based on bi-abduction. This work constitutes a breakthrough, in that it is now possible prove properties about millions of lines of code, thus making the reasoning viable for industry. Facebook will run a lab on Infer on 14th November. 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
-Time Mondays 2pm-4pm, 2nd--9th week
-Coursework Published: Monday 7th of November
-Submitted: Wednesday 16th of November
-Feedback: Monday 21st of November
-Exam 11th week
-Recommended Reading: Mike Gordon has some excellent notes on Hoare logic, which briefly touches on separation logic in the last chapter. Two good books on Hoare logic are: Logic in Computer Science: Modelling and Reasoning
-about Systems, Michael Huth and Mark Ryan, CUP, 2004; and The Formal Semantics of Programming Languages: an Introduction, Glynn Winskel, MIT Press, 1993.
-
-Most of the work on separation logic is in research papers. Excellent introductions to separation logic include: O'Hearn, Reynolds and Yang's paper on Local Reasoning about Programs that Alter Data Structures, CSL 2001, and John Reynolds' undergraduate course notes on separation logic and survey paper Separation Logic: A Logic for Shared Mutable Data Structures, LICS 2002, both found on Reynolds' homepage. Andrew Appel has published a book on Program Logics for Certified Compilers}, CUP 2014 (a copy is available in the library).
-
-Papers describing tool techniques include: Symbolic Execution with Separation Logic}, Berdine, Calcagno, O'Hearn, APLAS'05; A Local Shape Analysis based on Separation Logic, Distefano, O'Hearn, Yang, TACAS
-2006; and Compositional Shape Analysis by Means of Bi-abduction, Calcagno, Distefano, O'Hearn, Yang, JACM 2011.
-
-The initial paper on concurrent separation logic is Resources, Concurrency and Local Reasoning, O'Hearn, TCS, 2007, and is worth a read. The paper paper Steps in Modular Specifications of Concurrent Modules, da Rocha Pinto, Dinsdale-Young, Gardner, MFPS 2015, describes some modern developments in concurrent separation logics. There are many additional interesting links given on the piazza site. If you have further suggestions on what reading material might be of interest, please let me know.
diff --git a/research/separationlogic.md b/research/separationlogic.md
new file mode 100644
index 0000000..4ca7597
--- /dev/null
+++ b/research/separationlogic.md
@@ -0,0 +1,57 @@
+---
+title: Separation Logic
+project_id: sl
+menu: true
+menu_order: 5
+---
+
+Separation Logic: Local Reasoning about Programs (404H)
+
+#### 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. 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.
+It has been used to reason about C, Java and JavaScript programs, and algorithms for shared-memory concurrency.
+There are many academic verification tools, such as Smallfoot, Verifast and Abductor, and the industrial tool [Infer](http://fbinfer.com/), developed by a team led by Peter O'Hearn at Facebook.
+As well as Facebook, Infer is used by Instagram, kiuwan, oculus, Spotify, UBER, WhatsApp, Marks and Spencer, and Sky.
+
+#### Course Outline
+
+The course comprises two hours a week for seven weeks.
+It will be accompanied by comprehensive course notes, which bring together a variety of ideas from the most influential research papers.
+
+The first four weeks will provide a basic introduction to separation logic for reasoning about mutable data structures, using linked lists and binary trees as the primary examples.
+You will learn how to write program specifications and prove properties of programs, both informally using sketch proofs and formally using rigorous proofs.
+The next two weeks will describe tools, demonstrating that reasoning about real-world programs using separation logic is feasible.
+You will learn about Smallfoot, a semi-automatic verification tool based on symbolic execution, and Infer, an automatic tool based on bi-abduction.
+This work constitutes a breakthrough, in that it is now possible prove properties about millions of lines of code, thus making the reasoning viable for industry.
+Facebook will run a lab on Infer on 14th November.
+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
+
+Time: Mondays 2pm-4pm, 2nd--9th week
+
+Coursework Published: Monday 7th of November
+
+Submitted: Wednesday 16th of November
+
+Feedback: Monday 21st of November
+
+Exam: 11th week
+
+Recommended Reading: Mike Gordon has some excellent notes on [Hoare logic](http://www.cl.cam.ac.uk/~mjcg/Teaching/2011/Hoare/Notes/Notes.pdf), which briefly touches on separation logic in the last chapter.
+Two good books on Hoare logic are: Logic in Computer Science: Modelling and Reasoning about Systems, Michael Huth and Mark Ryan, CUP, 2004; and The Formal Semantics of Programming Languages: an Introduction, Glynn Winskel, MIT Press, 1993.
+
+Most of the work on separation logic is in research papers.
+Excellent introductions to separation logic include: O'Hearn, Reynolds and Yang's paper on [Local Reasoning about Programs that Alter Data Structures](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/localreasoning.pdf), CSL 2001, and John Reynolds' undergraduate course notes on separation logic and survey paper [Separation Logic: A Logic for Shared Mutable Data Structures](https://www.cs.cmu.edu/~jcr/seplogic.pdf), LICS 2002, both found on Reynolds' homepage.
+Andrew Appel has published a book on Program Logics for Certified Compilers, CUP 2014 (a copy is available in the [library](http://www.imperial.ac.uk/admin-services/library/)).
+
+Papers describing tool techniques include: [Symbolic Execution with Separation Logic](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.64.2006&rep=rep1&type=pdf), Berdine, Calcagno, O'Hearn, APLAS'05; [A Local Shape Analysis based on Separation Logic](http://www.eecs.qmul.ac.uk/~ddino/papers/localshape.pdf), Distefano, O'Hearn, Yang, TACAS 2006; and Compositional Shape Analysis by Means of Bi-abduction, Calcagno, Distefano, O'Hearn, Yang, JACM 2011.
+
+The initial paper on concurrent separation logic is [Resources, Concurrency and Local Reasoning](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf), O'Hearn, TCS, 2007, and is worth a read.
+The survey paper [Steps in Modular Specifications of Concurrent Modules](https://www.doc.ic.ac.uk/~pg/papers/mfps15.pdf), da Rocha Pinto, Dinsdale-Young, Gardner, MFPS 2015, describes some modern developments in concurrent separation logics.
+There are many additional interesting links given on the [Piazza](https://piazza.com) site.
+If you have further suggestions on what reading material might be of interest, please let us know.
--
GitLab