Search

• < Previous
• 1
• Next >

---

Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency

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&nbsp;[&hellip;]

---

Permission-Based Separation Logic for Message-Passing Concurrency

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&nbsp;[&hellip;]

---

Bidirectional Runtime Enforcement of First-Order Branching-Time Properties

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&nbsp;[&hellip;]

---

Complexity results for modal logic with recursion via translations and tableaux

Luca Aceto ; Antonis Achilleos ; Elli Anastasiadi ; Adrian Francalanza ; Anna Ingólfsdóttir.

This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the $\mu$-calculus and modal&nbsp;[&hellip;]

---