3 results
Adrian Francalanza ; Edsko DeVries ; Matthew Hennessy.
We define a pi-calculus variant with a costed semantics where channels are treated as resources that must explicitly be allocated before they are used and can be deallocated when no longer required. We use a substructural type system tracking permission transfer to construct coinductive proof […]
Published on June 26, 2014
Adrian Francalanza ; Julian Rathke ; Vladimiro Sassone.
We develop local reasoning techniques for message passing concurrent programs based on ideas from separation logics and resource usage analysis. We extend processes with permission- resources and define a reduction semantics for this extended language. This provides a foundation for interpreting […]
Published on September 1, 2011
Luca Aceto ; Ian Cassar ; Adrian Francalanza ; Anna Ingolfsdottir.
Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an […]
Published on February 28, 2023