12 citations · 30 across the 10 of their papers we have counts for
14 papers
Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
Marcos Grandury, Aleksandar Nanevski, Alexander Gryzlov
Verifying graph algorithms has long been considered challenging in separation logic, mainly due to structural sharing between graph subcomponents. We show that these challenges can…
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack: Extended Version
Jesús Domínguez, Aleksandar Nanevski
Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms' linearization points (LP). However, LPs often hinder…
Declarative Linearizability Proofs for Descriptor-Based Concurrent Helping Algorithms
Jesús Domínguez, Aleksandar Nanevski
Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms' linearization points. However, relying on linearizat…
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…
Proving Highly-Concurrent Traversals Correct
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea +4
Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any sy…
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…
Concurrent Data Structures Linked in Time
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski +1
Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data stru…
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee +1
Designing scalable concurrent objects, which can be efficiently used on multicore processors, often requires one to abandon standard specification techniques, such as linearizabili…
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
We present a lightweight approach to Hoare-style specifications for fine-grained concurrency, based on a notion of time-stamped histories that abstractly capture atomic changes in…
Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
Murdoch Gabbay, Aleksandar Nanevski
The modal logic S4 can be used via a Curry-Howard style correspondence to obtain a lambda-calculus. Modal (boxed) types are intuitively interpreted as `closed syntax of the calculu…