Aleksandar Nanevski

54 papers A* 6A 13B 1C 2Journal 29Unranked 3
YearRankTypeTitle / Venue / Authors
2025 J jnl
Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version).
CoRR
Marcos Grandury, Aleksandar Nanevski, Alexander Gryzlov
2025 J jnl
Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach.
Proc. ACM Program. Lang.
Marcos Grandury, Aleksandar Nanevski, Alexander Gryzlov
2023 J jnl
Declarative Linearizability Proofs for Descriptor-Based Concurrent Helping Algorithms.
CoRR
Jesús Domínguez, Aleksandar Nanevski
2023 B conf
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack.
CONCUR
Jesús Domínguez, Aleksandar Nanevski
2023 J jnl
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack: Extended Version.
CoRR
Jesús Domínguez, Aleksandar Nanevski
2022 J jnl
Visibility reasoning for concurrent snapshot algorithms.
Proc. ACM Program. Lang.
Joakim Öhman, Aleksandar Nanevski
2021 J jnl
Contextual Modal Types for Algebraic Effects and Handlers.
CoRR
Nikita Zyuzin, Aleksandar Nanevski
2021 J jnl
Contextual modal types for algebraic effects and handlers.
Proc. ACM Program. Lang.
Nikita Zyuzin, Aleksandar Nanevski
2021 J jnl
On algebraic abstractions for concurrent separation logics.
Proc. ACM Program. Lang.
Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
2021 J jnl
Visibility Reasoning for Concurrent Snapshot Algorithms.
CoRR
Joakim Öhman, Aleksandar Nanevski
2020 J jnl
On Algebraic Abstractions for Concurrent Separation Logics.
CoRR
Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
2020 J jnl
Proving Highly-Concurrent Traversals Correct.
CoRR
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham
2020 J jnl
Proving highly-concurrent traversals correct.
Proc. ACM Program. Lang.
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham
2019 J jnl
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations.
CoRR
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
2019 J jnl
Specifying concurrent programs in separation logic: morphisms and simulations.
Proc. ACM Program. Lang.
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
2017 J jnl
Concurrent Data Structures Linked in Time (Artifact).
Dagstuhl Artifacts Ser.
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2017 A conf
Concurrent Data Structures Linked in Time.
ECOOP
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2017 J jnl
Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources.
CoRR
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
2016 J jnl
Concurrent Data Structures Linked in Time.
CoRR
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2016 A conf
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects.
OOPSLA
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
2016 J jnl
Operational Aspects of C/C++ Concurrency.
CoRR
Anton Podkopaev, Ilya Sergey, Aleksandar Nanevski
2015 J jnl
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects.
CoRR
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
2015 A* conf
Mechanized verification of fine-grained concurrent programs.
PLDI
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2015 J jnl
Mtac: A monad for typed tactic programming in Coq.
J. Funct. Program.
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
2015 A conf
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity.
ESOP
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2014 A conf
Communicating State Transition Systems for Fine-Grained Concurrent Resources.
ESOP
Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco
2014 A* conf
Modular reasoning about heap paths via effectively propositional formulas.
POPL
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv
2014 J jnl
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity.
CoRR
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2013 J jnl
Denotation of contextual modal type theory (CMTT): Syntax and meta-programming.
J. Appl. Log.
Murdoch James Gabbay, Aleksandar Nanevski
2013 J jnl
Dependent Type Theory for Verification of Information Flow and Access Control Policies.
ACM Trans. Program. Lang. Syst.
Aleksandar Nanevski, Anindya Banerjee, Deepak Garg
2013 C conf
Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures.
PPDP
Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski
2013 A* conf
Effectively-Propositional Reasoning about Reachability in Linked Data Structures.
CAV
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv
2013 A conf
Hoare-style reasoning with (algebraic) continuations.
ICFP
Germán Andrés Delbianco, Aleksandar Nanevski
2013 J jnl
How to make ad hoc proof automation less ad hoc.
J. Funct. Program.
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer
2013 A conf
Mtac: a monad for typed tactic programming in Coq.
ICFP
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
2013 A* conf
Subjective auxiliary state for coarse-grained concurrency.
POPL
Ruy Ley-Wild, Aleksandar Nanevski
2012 J jnl
Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
CoRR
Murdoch Gabbay, Aleksandar Nanevski
2011 A conf
How to make ad hoc proof automation less ad hoc.
ICFP
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer
2011 — conf
Partiality, State and Dependent Types.
TLCA
Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski
2011 A* conf
Verification of Information Flow and Access Control Policies with Dependent Types.
IEEE Symposium on Security and Privacy
Aleksandar Nanevski, Anindya Banerjee, Deepak Garg
2010 A* conf
Structuring the verification of heap-manipulating programs.
POPL
Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine
2009 — conf
Towards type-theoretic semantics for transactional concurrency.
TLDI
Aleksandar Nanevski, Paul Govereau, Greg Morrisett
2008 A conf
A Realizability Model for Impredicative Hoare Type Theory.
ESOP
Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett
2008 J jnl
Contextual modal type theory.
ACM Trans. Comput. Log.
Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka
2008 J jnl
Hoare type theory, polymorphism and separation.
J. Funct. Program.
Aleksandar Nanevski, J. Gregory Morrisett, Lars Birkedal
2008 A conf
Ynot: dependent types for imperative programs.
ICFP
Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal
2007 A conf
Abstract Predicates and Mutable ADTs in Hoare Type Theory.
ESOP
Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal
2006 A conf
Polymorphism and separation in hoare type theory.
ICFP
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
2005 J jnl
Staged computation with names and necessity.
J. Funct. Program.
Aleksandar Nanevski, Frank Pfenning
2003 — conf
A modal foundation for meta-variables.
MERLIN
Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning
2003 J jnl
Automatic Generation of Staged Geometric Predicates.
High. Order Symb. Comput.
Aleksandar Nanevski, Guy E. Blelloch, Robert Harper
2003 C conf
From dynamic binding to state via modal possibility.
PPDP
Aleksandar Nanevski
2002 A conf
Meta-programming with names and necessity.
ICFP
Aleksandar Nanevski
2001 A conf
Automatic Generation of Staged Geometric Predicates.
ICFP
Aleksandar Nanevski, Guy E. Blelloch, Robert Harper