Aleksandar Nanevski

Cited by

	All	Since 2016
Citations	2194	911
h-index	23	16
i10-index	33	22

240

120

180

200320042005200620072008200920102011201220132014201520162017201820192020202119 21 24 28 69 105 104 117 126 113 171 165 189 151 239 165 205 136 15

Co-authors

Anindya BanerjeeProfessor, IMDEA Software InstituteVerified email at imdea.org
Greg MorrisettDean and Professor, Cornell UniversityVerified email at cornell.edu
Lars BirkedalDept. of Computer Science, Aarhus UniversityVerified email at cs.au.dk
Ilya SergeyYale-NUS College and National University of SingaporeVerified email at yale-nus.edu.sg
Germán DelbiancoNomadic LabsVerified email at nomadic-labs.com
Frank PfenningProfessor of Computer Science, Carnegie Mellon UniversityVerified email at cs.cmu.edu
Brigitte PientkaMcGill UniversityVerified email at cs.mcgill.ca
Beta ZilianiFAMAF, UNC and CONICETVerified email at mpi-sws.org
Derek DreyerMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics CampusVerified email at mpi-sws.org
Viktor VafeiadisMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics Campus (SIC)Verified email at mpi-sws.org
Deepak GargMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics Campus (SIC)Verified email at mpi-sws.org
Shachar ItzhakyTel Aviv UniversityVerified email at tau.ac.il
Mooly SagivTel Aviv UniversityVerified email at acm.org
Neil ImmermanCollege of Computer and Information Sciences, UMass, AmherstVerified email at cs.umass.edu
Georges GonthierPrincipal Researcher, Microsoft ResearchVerified email at microsoft.com
Neelakantan R. KrishnaswamiUniversity of CambridgeVerified email at cl.cam.ac.uk
Josh BerdineFacebookVerified email at fb.com
Amal AhmedNortheastern UniversityVerified email at ccs.neu.edu
Edmund ClarkeUniversity Professor Emeritus at Carnegie Mellon UniversityVerified email at cs.cmu.edu
Stephen MagillGalois, Inc.Verified email at galois.com

Aleksandar Nanevski

IMDEA Software Institute

Verified email at imdea.org - Homepage

Logic and Programming Languages


Title Sort by citations Sort by year Sort by title	Cited by Cited by	Year
Contextual modal type theory A Nanevski, F Pfenning, B Pientka ACM Transactions on Computational Logic (TOCL) 9 (3), 1-49, 2008	292	2008
Ynot: dependent types for imperative programs A Nanevski, G Morrisett, A Shinnar, P Govereau, L Birkedal Proceedings of the 13th ACM SIGPLAN international conference on Functional …, 2008	243*	2008
Polymorphism and separation in Hoare type theory A Nanevski, G Morrisett, L Birkedal ACM SIGPLAN Notices 41 (9), 62-73, 2006	160	2006
Hoare type theory, polymorphism and separation. A Nanevski, JG Morrisett, L Birkedal J. Funct. Program. 18 (5-6), 865-911, 2008	152	2008
Communicating state transition systems for fine-grained concurrent resources A Nanevski, R Ley-Wild, I Sergey, GA Delbianco European Symposium on Programming Languages and Systems, 290-310, 2014	108	2014
Verification of information flow and access control policies with dependent types A Nanevski, A Banerjee, D Garg 2011 IEEE Symposium on Security and Privacy, 165-179, 2011	107	2011
Mechanized verification of fine-grained concurrent programs I Sergey, A Nanevski, A Banerjee Proceedings of the 36th ACM SIGPLAN Conference on Programming Language …, 2015	103	2015
Structuring the verification of heap-manipulating programs A Nanevski, V Vafeiadis, J Berdine Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010	79	2010
Mtac: A monad for typed tactic programming in Coq B Ziliani, D Dreyer, NR Krishnaswami, A Nanevski, V Vafeiadis ACM SIGPLAN Notices 48 (9), 87-100, 2013	76	2013
Abstract predicates and mutable ADTs in Hoare type theory A Nanevski, A Ahmed, G Morrisett, L Birkedal European Symposium on Programming, 189-204, 2007	75	2007
Inferring invariants in separation logic for imperative list-processing programs S Magill, A Nanevski, E Clarke, P Lee SPACE 1 (1), 5.7, 2006	74	2006
Meta-programming with names and necessity A Nanevski ACM SIGPLAN Notices 37 (9), 206-217, 2002	71	2002
Subjective auxiliary state for coarse-grained concurrency R Ley-Wild, A Nanevski Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013	62	2013
Effectively-propositional reasoning about reachability in linked data structures S Itzhaky, A Banerjee, N Immerman, A Nanevski, M Sagiv International Conference on Computer Aided Verification, 756-772, 2013	59	2013
How to make ad hoc proof automation less ad hoc G Gonthier, B Ziliani, A Nanevski, D Dreyer ACM SIGPLAN Notices 46 (9), 163-175, 2011	59	2011
Dependent type theory for verification of information flow and access control policies A Nanevski, A Banerjee, D Garg ACM Transactions on Programming Languages and Systems (TOPLAS) 35 (2), 1-41, 2013	54	2013
Specifying and verifying concurrent algorithms with histories and subjectivity I Sergey, A Nanevski, A Banerjee European Symposium on Programming Languages and Systems, 333-358, 2015	51	2015
Staged computation with names and necessity A Nanevski, F Pfenning Carnegie Mellon University, 2002	42	2002
Modular reasoning about heap paths via effectively propositional formulas S Itzhaky, A Banerjee, N Immerman, O Lahav, A Nanevski, M Sagiv ACM SIGPLAN Notices 49 (1), 385-396, 2014	36	2014
A realizability model for impredicative Hoare Type Theory RL Petersen, L Birkedal, A Nanevski, G Morrisett European Symposium on Programming, 337-352, 2008	36	2008

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Upload PDF

Follow this author

Cited by

Co-authors