12 citations · 30 across the 10 of their papers we have counts for
7 papers · 1 filter
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…
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…