| 2023 | CONCUR | Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack. | Jess Domnguez, Aleksandar Nanevski |
| 2017 | ECOOP | Concurrent Data Structures Linked in Time. | Germn Andrs Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee |
| 2016 | OOPSLA | Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. | Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germn Andrs Delbianco |
| 2015 | ESOP | Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. | Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee |
| 2015 | PLDI | Mechanized verification of fine-grained concurrent programs. | Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee |
| 2014 | ESOP | Communicating State Transition Systems for Fine-Grained Concurrent Resources. | Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germn Andrs Delbianco |
| 2014 | POPL | Modular reasoning about heap paths via effectively propositional formulas. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv |
| 2013 | CAV | Effectively-Propositional Reasoning about Reachability in Linked Data Structures. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv |
| 2013 | ICFP | Hoare-style reasoning with (algebraic) continuations. | Germn Andrs Delbianco, Aleksandar Nanevski |
| 2013 | ICFP | Mtac: a monad for typed tactic programming in Coq. | Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis |
| 2013 | POPL | Subjective auxiliary state for coarse-grained concurrency. | Ruy Ley-Wild, Aleksandar Nanevski |
| 2013 | PPDP | Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. | Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski |
| 2011 | ICFP | How to make ad hoc proof automation less ad hoc. | Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer |
| 2011 | SP | Verification of Information Flow and Access Control Policies with Dependent Types. | Aleksandar Nanevski, Anindya Banerjee, Deepak Garg |
| 2010 | POPL | Structuring the verification of heap-manipulating programs. | Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine |
| 2008 | ESOP | A Realizability Model for Impredicative Hoare Type Theory. | Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett |
| 2008 | ICFP | Ynot: dependent types for imperative programs. | Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal |
| 2007 | ESOP | Abstract Predicates and Mutable ADTs in Hoare Type Theory. | Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal |
| 2006 | ICFP | Polymorphism and separation in hoare type theory. | Aleksandar Nanevski, Greg Morrisett, Lars Birkedal |
| 2003 | ICFP | A modal foundation for meta-variables. | Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning |
| 2003 | PPDP | From dynamic binding to state via modal possibility. | Aleksandar Nanevski |
| 2002 | ICFP | Meta-programming with names and necessity. | Aleksandar Nanevski |
| 2001 | ICFP | Automatic Generation of Staged Geometric Predicates. | Aleksandar Nanevski, Guy E. Blelloch, Robert Harper |