Aleksandar Nanevski

Assistant 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

My research interest is in the design and implementation of programming languages and methodologies that facilitate specification and verification of various program properties. My recent focus has been on the design of a programming language which integrates the well-known program logics, like Hoare and Separation Logic, with modern programming features for abstraction, information hiding and code reuse, such as higher-order functions, monads, polymorphism and modules.

I am also interested in all aspects of compilation and optimization of such languages, and in other formal verification methods, such as interactive and automated theorem proving, decision procedures, program analysis and software model checking.

Professional activities

Publications

Communicating State Transition Systems for Fine-Grained Concurrent Resources
Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey and German Andres Delbianco
Proceedings of ESOP'14, pages 290-310, 2014.
Associated Coq scripts can be downloaded here.

Modular Reasoning about Heap Paths via Effectively Propositional Formulas
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski and Mooly Sagiv
Proceedings of POPL'14, pages 385-396, 2014.

Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures
Gordon Stewart, Anindya Banerjee and Aleksandar Nanevski
Proceedings of PPDP'13, pages 145-156, 2013.
Associated Coq scripts can be downloaded here.

Hoare-Style Reasoning with (Algebraic) Continuations
German Andres Delbianco and Aleksandar Nanevski
Proceedings of ICFP'13, pages 363-376, 2013.
Associated Coq scripts can be downloaded here.

Mtac: A Monad for Typed Tactic Programming in Coq
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski and Viktor Vafeiadis
Proceedings of ICFP'13, pages 87-100, 2013.
Associated Coq scripts can be downloaded here.

Effectively-Propositional Reasoning about Reachability in Linked Data Structures
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski and Mooly Sagiv
Proceedings of CAV'13, pages 756-772, 2013.

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.
Associated Coq scripts can be downloaded here.

Subjective Auxiliary State for Coarse-Grained Concurrency
Ruy Ley-Wild and Aleksandar Nanevski
Proceedings of POPL'13, pages 561-574, 2013.
Associated Coq scripts can be downloaded here.

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.
Associated Coq scripts can be downloaded here.
Online appendix with the proof rules is here.

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.

How to Make Ad Hoc Proof Automation Less Ad Hoc
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski and Derek Dreyer
Proceedings of ICFP'11, pages 163-175, 2011.
Associated Coq scripts and technical appendix can be downloaded here.

Verification of Information Flow and Access Control Policies with Dependent Types
Aleksandar Nanevski, Anindya Banerjee and Deepak Garg
Proceedings of S&P'11, pages 165-179, 2011.
Extended version available as a technical report.
Associated Coq scripts can be downloaded here.

Partiality, State and Dependent Types
Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski
Proceedings of TLCA'11, pages 198-212, 2011.
Extended version available as a technical report.
Associated Coq scripts can be downloaded here.

Structuring the Verification of Heap-Manipulating Programs
Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine
Proceedings of POPL'10, pages 261-274, 2010.
Associated Coq scripts can be downloaded here.

Towards Type-theoretic Semantics for Transactional Concurrency
Aleksandar Nanevski, Paul Govereau, Greg Morrisett
Proceedings of TLDI'09, pages 79-90, 2009.
Extended version available as technical report TR-09-07, Harvard University.

Ynot: Dependent Types for Imperative Programs
Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau, Lars Birkedal.
Proceedings of ICFP'08, pages 229-240, 2008.
The examples from this paper can be downloaded from here.

A Realizability Model for Impredicative Hoare Type Theory
Rasmus L. Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett
Proceedings of ESOP'08, pages 337-352, 2008.

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

Hoare Type Theory, Polymorphism and Separation
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
Journal of Functional Programming (JFP), 18(5&6):865-911, September 2008.
Extended version of the ICFP'06 paper.

Abstract Predicates and Mutable ADTs in Hoare Type Theory
Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal
Proceedings of ESOP'07, pages 189-204, 2007.
Extended version available as technical report TR-14-06, Harvard University.

Polymorphism and Separation in Hoare Type Theory
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
Proceedings of ICFP'06, pages 62-73, 2006.
Extended version available as technical report TR-10-06, Harvard University.

Inferring Invariants in Separation Logic for Imperative List-processing Programs
Stephen Magill, Aleksandar Nanevski, Edmund Clarke and Peter Lee
Proceedings of SPACE'06, pages 47-60, January 2006.

Dependent Type Theory of Stateful Higher-Order Functions
Aleksandar Nanevski, Greg Morrisett
Extended version available as technical report TR-24-05, Harvard University, 2005.

A Modal Calculus for Exception Handling
Aleksandar Nanevski
Proceedings of IMLA'05, June 2005.

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

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

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

A Modal Foundation for Meta-Variables
Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning
Proceedings of MERLIN'03, pages 159-170, 2003.

From Dynamic Binding to State via Modal Possibility
Aleksandar Nanevski
Proceedings of PPDP'03, pages 207-218, 2003.

A Nominal Modal Calculus of Effects
Aleksandar Nanevski
Technical Report CMU-CS-03-149, Carnegie Mellon University, June 2003.
Shorter version available here.
Interpreter for effect systems presented in this report and the PPDP'03 paper.

Meta-Programming with Names and Necessity
Aleksandar Nanevski
Proceedings of ICFP'02, pages 206-217, 2002. Slides.
Superseded by the technical report CMU-CS-02-123R, November 2002.

Automatic Generation of Staged Geometric Predicates
Aleksandar Nanevski, Guy Blelloch, Robert Harper
Proceedings of ICFP'01, pages 217-228, 2001. Slides.
Extended version available as technical report CMU-CS-01-141, June 2001.