Aleksandar Nanevski


Research Professor

IMDEA Software Institute
Edificio IMDEA Software, office 382
Campus Montegancedo UPM
28223 Pozuelo de Alarcon, Madrid
SPAIN

email:
phone: +34-91-101-2202 (ext: 4107)
fax: +34-91-101-1358

Research interests

My research is in the design and implementation of programming languages and logics for software verification. More specifically, I am interested in applying programming methodology to facilitate the construction of formal proofs in mathematics in general, and of program correctness in particular. My recent focus has been on designing methods for integrating programming with pointers, concurrency, and other important imperative features, into dependent type systems such as that of the proof assistant Coq. The goal of the integration is to leverage the proving power of Coq to obtain effective and scalable ways for reasoning about security and correctness of imperative programs.

I am also interested in all other aspects of formal mathematics and programming language theory and applications related to compilation, optimization, semantics, interactive theorem proving, program extraction, automated deduction, decision procedures, program analysis and model checking.

Group

Current members

Former members

Professional activities

Publications

Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack
Jesús Domínguez and Aleksandar Nanevski
International Conference on Concurrency Theory (CONCUR), 2023.
[pdf | doi | extended version]

Declarative Linearizability Proofs for Descriptor-Based Concurrent Helping Algorithms
Jesús Domínguez and Aleksandar Nanevski
[arxiv]

Visibility Reasoning for Concurrent Snapshot Algorithms
Joakim Öhman and Aleksandar Nanevski
Symposium on Principles of Programming Languages (POPL), 2022.
[pdf | doi | extended version]

Contextual Modal Types for Algebraic Effects and Handlers
Nikita Zyuzin and Aleksandar Nanevski
International Conference on Functional Programming (ICFP), 2021.
[pdf | doi | extended version]

On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco and Ignacio Fábregas
Symposium on Principles of Programming Languages (POPL), 2021.
[pdf | doi | extended version | project page]

Proving Highly-Concurrent Traversals Correct
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky and Sharon Shoham
International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 128:1--128:29, 2020.
[pdf | doi]

Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco and Ignacio Fábregas
International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 161:1-161:30, 2019.
[pdf | doi | extended version | project page]

Concurrent Data Structures Linked in Time
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee
European Conference on Object-Oriented Programming (ECOOP), pages 8:1-8:30, 2017
[pdf | doi | project page]

Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee and Germán Andrés Delbianco
International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 92-110, 2016.
[pdf | doi | project page]

Separation Logic and Concurrency
Aleksandar Nanevski
Lecture notes for Oregon Programming Languages Summer School (OPLSS), June 2016.
[pdf | oplss16 page]

Operational Aspects of C/C++ Concurrency
Anton Podkopaev, Ilya Sergey and Aleksandar Nanevski
[arxiv]

Mtac: A Monad for Typed Tactic Programming in Coq
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski and Viktor Vafeiadis
Journal of Functional Programming (JFP), April 2015.
[pdf | doi | icfp13 version]

Mechanized Verification of Fine-grained Concurrent Programs
Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee
Conference on Programming Language Design and Implementation (PLDI), pages 77-87, 2015.
[pdf | doi | coq sources | project page]

Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee
European Symposium on Programming (ESOP), pages 333-358, 2015.
[pdf | doi | extended version | project page]

Communicating State Transition Systems for Fine-Grained Concurrent Resources
Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey and Germán Andrés Delbianco
European Symposium on Programming (ESOP), pages 290-310, 2014.
[pdf | doi | coq cources | project page]

Modular Reasoning about Heap Paths via Effectively Propositional Formulas
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski and Mooly Sagiv
Symposium on Principles of Programming Languages (POPL), pages 385-396, 2014.
[pdf | doi]

Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures
Gordon Stewart, Anindya Banerjee and Aleksandar Nanevski
Symposium on Principles and Practice of Declarative Programming (PPDP), pages 145-156, 2013.
[pdf | doi | coq sources | project page]

Hoare-Style Reasoning with (Algebraic) Continuations
Germán Andrés Delbianco and Aleksandar Nanevski
International Conference on Functional Programming (ICFP), pages 363-376, 2013.
[pdf | doi | coq sources]

Mtac: A Monad for Typed Tactic Programming in Coq
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski and Viktor Vafeiadis
International Conference on Functional Programming (ICFP), pages 87-100, 2013.
[pdf | doi | coq sources]

Effectively-Propositional Reasoning about Reachability in Linked Data Structures
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski and Mooly Sagiv
International Conference on Computer Aided Verification (CAV), pages 756-772, 2013.
[pdf | doi]

How to Make Ad Hoc Proof Automation Less Ad Hoc
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski and Derek Dreyer
Journal of Functional Programming (JFP), 23(4):357-401, July 2013.
[pdf | doi | coq sources | icfp11 version]

Subjective Auxiliary State for Coarse-Grained Concurrency
Ruy Ley-Wild and Aleksandar Nanevski
Symposium on Principles of Programming Languages (POPL), pages 561-574, 2013.
[pdf | doi | coq sources | online appendix | project page]

Dependent Type Theory for Verification of Information Flow and Access Control Policies
Aleksandar Nanevski, Anindya Banerjee, Deepak Garg
ACM Transactions on Programming Languages and Systems (TOPLAS), 35(2):6:1-6:41, July 2013.
[pdf | doi | coq sources | online appendix | s&p11 version | Project page]

Denotation of contextual modal type theory (CMTT): syntax and metaprogramming
Murdoch J. Gabbay and Aleksandar Nanevski
Journal of Applied Logic (JAPPL), 11(1):1-29, March 2013.
[pdf | doi]

How to Make Ad Hoc Proof Automation Less Ad Hoc
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski and Derek Dreyer
International Conference on Functional Programming (ICFP), pages 163-175, 2011.
[pdf | doi | coq sources]

Verification of Information Flow and Access Control Policies with Dependent Types
Aleksandar Nanevski, Anindya Banerjee and Deepak Garg
IEEE Symposium on Security and Privacy (S&P), pages 165-179, 2011.
[pdf | doi | extended version | coq sources | project page]

Partiality, State and Dependent Types
Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski
International Conference on Typed Lambda Calculi and Applications (TLCA), pages 198-212, 2011.
[pdf | doi | extended version | coq sources | project page]

Structuring the Verification of Heap-Manipulating Programs
Aleksandar Nanevski, Viktor Vafeiadis and Josh Berdine
Symposium on Principles of Programming Languages (POPL), pages 261-274, 2010.
[pdf | doi | coq sources | project page]

Towards Type-theoretic Semantics for Transactional Concurrency
Aleksandar Nanevski, Paul Govereau and Greg Morrisett
Workshop on Types in Language Design and Implementation (TLDI), pages 79-90, 2009.
[pdf | doi | extended version]

A Realizability Model for Impredicative Hoare Type Theory
Rasmus L. Petersen, Lars Birkedal, Aleksandar Nanevski and Greg Morrisett
European Symposium on Programming (ESOP), pages 337-352, 2008.
[pdf | doi | project page]

Ynot: Dependent Types for Imperative Programs
Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau and Lars Birkedal
International Conference on Functional Programming (ICFP), pages 229-240, 2008.
[pdf | doi | examples in Coq | project page]

Contextual Modal Type Theory
Aleksandar Nanevski, Frank Pfenning and Brigitte Pientka
ACM Transactions on Computational Logic (TOCL), 9(3):1-49, June 2008.
[pdf | doi]

Hoare Type Theory, Polymorphism and Separation
Aleksandar Nanevski, Greg Morrisett and Lars Birkedal
Journal of Functional Programming (JFP), 18(5&6):865-911, September 2008.
[pdf | doi | icfp06 version | project page]

Abstract Predicates and Mutable ADTs in Hoare Type Theory
Aleksandar Nanevski, Amal Ahmed, Greg Morrisett and Lars Birkedal
European Symposium on Programming (ESOP), pages 189-204, 2007.
[pdf | doi | tr-14-06 | project page]

Polymorphism and Separation in Hoare Type Theory
Aleksandar Nanevski, Greg Morrisett and Lars Birkedal
International Conference on Functional Programming (ICFP), pages 62-73, 2006.
[pdf | doi | tr-10-06 | project page]

Inferring Invariants in Separation Logic for Imperative List-processing Programs
Stephen Magill, Aleksandar Nanevski, Edmund Clarke and Peter Lee
Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE), pages 47-60, 2006.
[pdf]

Dependent Type Theory of Stateful Higher-Order Functions
Aleksandar Nanevski and Greg Morrisett
Technical report TR-24-05, Harvard University, 2005.
[pdf | extended version | project page]

A Modal Calculus for Exception Handling
Aleksandar Nanevski
Workshop on Intuitionistic Modal Logic and Applications (IMLA), 2005.
[pdf]

Staged Computation with Names and Necessity
Aleksandar Nanevski and Frank Pfenning
Journal of Functional Programming (JFP), 15(6):893-939, November 2005.
[pdf | doi]

Functional Programming with Names and Necessity
Aleksandar Nanevski
PhD thesis, Carnegie Mellon University, 2004.
[pdf]

Automatic Generation of Staged Geometric Predicates
Aleksandar Nanevski, Guy Blelloch and Robert Harper
Higher-Order and Symbolic Computation (HOSC), 16(4):379-400, December 2003.
[pdf | doi | icfp01 version]

A Modal Foundation for Meta-Variables
Aleksandar Nanevski, Brigitte Pientka and Frank Pfenning
Workshop on Mechanized reasoning about languages with variable binding (MERLIN), pages 159-170, 2003.
[pdf | doi]

From Dynamic Binding to State via Modal Possibility
Aleksandar Nanevski
Symposium on Principles and Practice of Declarative Programming (PPDP), pages 207-218, 2003.
[pdf | doi]

A Modal Calculus for Effect Handling
Aleksandar Nanevski
Technical Report CMU-CS-03-149, Carnegie Mellon University, 2003.
[pdf | long version | short version | interpreter]

Meta-Programming with Names and Necessity
Aleksandar Nanevski
International Conference on Functional Programming (ICFP), pages 206-217, 2002.
[pdf | doi | superseding tr | slides]

Automatic Generation of Staged Geometric Predicates
Aleksandar Nanevski, Guy Blelloch and Robert Harper
International Conference on Functional Programming (ICFP), pages 217-228, 2001.
[pdf | doi | extended version | slides]