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

How to Make Ad Hoc Proof Automation Less Ad Hoc
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski and Derek Dreyer
Submitted for publication, December 2012.
Extended version of the ICFP'11 paper.
Associated Coq scripts can be downloaded here.

Subjective Auxiliary State for Coarse-Grained Concurrency
Ruy Ley-Wild and Aleksandar Nanevski
Proceedings of POPL'13. To appear.
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
Submitted for publication. May 2012.
Associated Coq scripts can be downloaded here.
Online appendix with the proof rules is here.

Dependent Types for Enforcement of Information Flow Policies in Data Structures
Gordon Stewart, Anindya Banerjee and Aleksandar Nanevski
Submitted for publication. May 2012.
Associated Coq scripts can be downloaded here.

Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
Murdoch J. Gabbay and Aleksandar Nanevski
To appear in Journal of Applied Logic (JAL). Submitted, January 2012. Accepted, June 2012.

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, Madrid, Spain, January 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, Savannah, GA, January 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, Victoria, Canada, September 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, Budapest, Hungary, April 2008.

Hoare Type Theory, Polymorphism and Separation
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
Journal of Functional Programming, 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, Braga, Portugal, March 2007.
Extended version available as technical report TR-14-06, Harvard University, September 2006.

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

Dependent Type Theory of Stateful Higher-Order Functions
Aleksandar Nanevski, Greg Morrisett
Extended version available as technical report TR-24-05, 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, Charleston, SC, January 2006.

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

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

A Nominal Modal Calculus of Effects
Aleksandar Nanevski
Technical Report CMU-CS-03-149, Carnegie Mellon University, June 2003.
Shorter version available here.

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

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

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

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

Meta-Programming with Names and Necessity
Supersedes the paper published in Proceedings of ICFP'02, Pittsburgh, PA, pages 206-217, October 2002.
Slides.

Automatic Generation of Staged Geometric Predicates
Aleksandar Nanevski, Guy Blelloch, Robert Harper
Higher-Order and Symbolic Computation, 16(4):379-400, December 2003.
Conference version appeared in Proceedings of ICFP 2001, Florence, Italy, pages 217-228, September 2001.
Slides. Extended version available as technical report CMU-CS-01-141, June 2001. PDF.

Software

Interpreter for effect systems presented in the papers on control flow effects and state.

Personal links | Macedonia FAQ