Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 10:36 - 10:58 at Sala II - Separation Logic and Memory Semantics Chair(s): Ilya Sergey

Precise management of resources and the obligations they impose, such as the need to dispose of memory, close locks, and release file handles, is hard—especially in the presence of concurrency, when some resources are shared, and different threads operate on them concurrently. We present Iron, a novel higher-order concurrent separation logic that allows for precise reasoning about resources that are transferable among dynamically allocated threads. In particular, Iron can be used to show the correctness of challenging examples, where the reclamation of memory is delegated to a forked-off thread. We show soundness of Iron by means of a model of Iron, defined on top of the Iris base logic, and we use this model to prove that memory resources are accounted for precisely and not leaked. We have formalized all of the developments in the Coq proof assistant.

Slides for Talk (slides.pdf)164KiB

Thu 17 Jan

Displayed time zone: Belfast change

10:36 - 12:04
Separation Logic and Memory SemanticsResearch Papers at Sala II
Chair(s): Ilya Sergey Yale-NUS College and National University of Singapore
10:36
22m
Talk
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Research Papers
Aleš Bizjak Aarhus University, Daniel Gratzer , Robbert Krebbers Delft University of Technology, Lars Birkedal Aarhus University
Link to publication DOI Media Attached File Attached
10:58
22m
Talk
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
Research Papers
José Fragoso Santos Imperial College London, Petar Maksimović Imperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Gabriela Sampaio Imperial College London, UK, Philippa Gardner Imperial College London
Link to publication DOI Media Attached File Attached
11:20
22m
Talk
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Research Papers
Alasdair Armstrong University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Alastair Reid Arm Ltd, Kathryn E. Gray University of Cambridge, Robert M. Norton University of Cambridge, Prashanth Mundkur SRI International, Mark Wassell University of Cambridge, Jon French University of Cambridge, Christopher Pulte University of Cambridge, Shaked Flur University of Cambridge, Ian Stark The University of Edinburgh, Neel Krishnaswami Computer Laboratory, University of Cambridge, Peter Sewell University of Cambridge
Link to publication DOI Media Attached File Attached
11:42
22m
Talk
Exploring C Semantics and Pointer Provenance
Research Papers
Kayvan Memarian University of Cambridge, Victor B. F. Gomes University of Cambridge, UK, Brooks Davis SRI International, Stephen Kell University of Kent, Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge, Peter Sewell University of Cambridge
Link to publication DOI Media Attached File Attached