15 citations · 37 across the 8 of their papers we have counts for
7 papers · 1 filter
Reasoning about External Calls
Sophia Drossopoulou, Julian Mackay, Susan Eisenbach +1
In today's complex software, internal trusted code is tightly intertwined with external untrusted code. To reason about internal code, programmers must reason about the potential e…
Reference Capabilities for Flexible Memory Management: Extended Version
Ellen Arvidsson, Elias Castegren, Sylvan Clebsch +4
Verona is a concurrent object-oriented programming language that organises all the objects in a program into a forest of isolated regions. Memory is managed locally for each region…
Necessity Specifications for Robustness
Julian Mackay, Sophia Drossopoulou, James Noble +1
Robust modules guarantee to do only what they are supposed to do - even in the presence of untrusted, malicious clients, and considering not just the direct behaviour of individual…
Holistic Specifications for Robust Programs
Sophia Drossopoulou, James Noble, Julian Mackay +1
Functional specifications describe what program components do: the sufficient conditions to invoke a component's operations. They allow us to reason about the use of components in…
Flint for Safer Smart Contracts
Franklin Schrans, Daniel Hails, Alexander Harkness +2
The Ethereum blockchain platform supports the execution of decentralised applications or smart contracts. These typically hold and transfer digital currency to other parties on the…
Safely Abstracting Memory Layouts
Juliana Franco, Alexandros Tasos, Sophia Drossopoulou +2
Modern architectures require applications to make effective use of caches to achieve high performance and hide memory latency. This in turn requires careful consideration of placem…
Behavioural types for non-uniform memory accesses
Juliana Franco, Sophia Drossopoulou
Concurrent programs executing on NUMA architectures consist of concurrent entities (e.g. threads, actors) and data placed on different nodes. Execution of these concurrent entities…