Aleksandar Nanevski

Cited by

	All	Since 2018
Citations	2654	967
h-index	25	17
i10-index	42	28

260

130

195

20032004200520062007200820092010201120122013201420152016201720182019202020212022202321 22 26 27 65 106 100 114 129 115 169 173 196 144 251 174 208 141 170 117 156

Public access

View all

23 articles

0 articles

available

not available

Based on funding mandates

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 SergeyAssociate Professor, National University of SingaporeVerified email at 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
Beta ZilianiFAMAF, UNC and Manas.TechVerified 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
Brigitte PientkaMcGill UniversityVerified email at cs.mcgill.ca
Deepak GargMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics Campus (SIC)Verified email at mpi-sws.org
Neelakantan R. KrishnaswamiUniversity of CambridgeVerified email at cl.cam.ac.uk
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
Murdoch GabbayLecturer in Computer Science at Heriot-Watt University, Edinburgh, UKVerified email at hw.ac.uk
Josh BerdineFacebookVerified email at fb.com
Edmund ClarkeUniversity Professor Emeritus at Carnegie Mellon UniversityVerified email at cs.cmu.edu
Stephen MagillSonatype, Inc.Verified email at sonatype.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	346	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	275*	2008
Polymorphism and separation in Hoare type theory A Nanevski, G Morrisett, L Birkedal ACM SIGPLAN Notices 41 (9), 62-73, 2006	184	2006
Hoare type theory, polymorphism and separation1 A Nanevski, G Morrisett, L Birkedal Journal of Functional Programming 18 (5-6), 865-911, 2008	174	2008
Mechanized verification of fine-grained concurrent programs I Sergey, A Nanevski, A Banerjee Proceedings of the 36th ACM SIGPLAN Conference on Programming Language …, 2015	141	2015
Communicating state transition systems for fine-grained concurrent resources A Nanevski, R Ley-Wild, I Sergey, GA Delbianco Programming Languages and Systems: 23rd European Symposium on Programming …, 2014	140	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	119	2011
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	86	2010
Inferring invariants in separation logic for imperative list-processing programs S Magill, A Nanevski, E Clarke, P Lee SPACE 1 (1), 5.7, 2006	86	2006
Abstract predicates and mutable ADTs in Hoare type theory A Nanevski, A Ahmed, G Morrisett, L Birkedal Programming Languages and Systems: 16th European Symposium on Programming …, 2007	77	2007
Meta-programming with names and necessity A Nanevski ACM SIGPLAN Notices 37 (9), 206-217, 2002	77	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	75	2013
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	69	2013
Specifying and verifying concurrent algorithms with histories and subjectivity I Sergey, A Nanevski, A Banerjee Programming Languages and Systems: 24th European Symposium on Programming …, 2015	67	2015
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	67	2011
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	65	2013
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	52	2013
Staged computation with names and necessity A Nanevski, F Pfenning Journal of Functional Programming 15 (6), 893-939, 2005	51	2005
Mtac: A monad for typed tactic programming in Coq B Ziliani, D Dreyer, NR Krishnaswami, A Nanevski, V Vafeiadis Journal of functional programming 25, e12, 2015	42	2015
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	41	2014

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

Follow

Cited by

Co-authors