3 papers
cs.PL2020
On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee +2
Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that…
cs.PL2019
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco +1
In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources---a form of state trans…
cs.PL2017
Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
Recent approaches to verifying programs in separation logics for concurrency have used state transition systems (STSs) to specify the atomic operations of programs. A key challenge…