12 citations · 30 across the 10 of their papers we have counts for
6 papers · 1 filter
Visibility Reasoning for Concurrent Snapshot Algorithms
Joakim Öhman, Aleksandar Nanevski
Visibility relations have been proposed by Henzinger et al. as an abstraction for proving linearizability of concurrent algorithms that obtains modular and reusable proofs. This is…
Contextual Modal Types for Algebraic Effects and Handlers
Nikita Zyuzin, Aleksandar Nanevski
Programming languages with algebraic effects often track the computations' effects using type-and-effect systems. In this paper, we propose to view an algebraic effect theory of a…
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…
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…
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…
Operational Aspects of C/C++ Concurrency
Anton Podkopaev, Ilya Sergey, Aleksandar Nanevski
In this work, we present a family of operational semantics that gradually approximates the realistic program behaviors in the C/C++11 memory model. Each semantics in our framework…