| Contextual modal type theory A Nanevski, F Pfenning, B Pientka ACM Transactions on Computational Logic (TOCL) 9 (3), 1-49, 2008 | 406 | 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 | 289* | 2008 |
| Polymorphism and separation in Hoare type theory A Nanevski, G Morrisett, L Birkedal ACM SIGPLAN Notices 41 (9), 62-73, 2006 | 187 | 2006 |
| Hoare type theory, polymorphism and separation1 A Nanevski, G Morrisett, L Birkedal Journal of Functional Programming 18 (5-6), 865-911, 2008 | 186 | 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 | 171 | 2015 |
| 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 | 160 | 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 | 123 | 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 | 95 | 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 | 88 | 2006 |
| 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 | 85 | 2013 |
| Meta-programming with names and necessity A Nanevski ACM SIGPLAN Notices 37 (9), 206-217, 2002 | 81 | 2002 |
| 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 | 77 | 2015 |
| Abstract predicates and mutable ADTs in Hoare type theory A Nanevski, A Ahmed, G Morrisett, L Birkedal European Symposium on Programming, 189-204, 2007 | 77 | 2007 |
| 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 | 76 | 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 | 73 | 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 | 72 | 2011 |
| 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 | 58 | 2013 |
| Staged computation with names and necessity A Nanevski, F Pfenning Journal of Functional Programming 15 (6), 893-939, 2005 | 58 | 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 | 50 | 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 | 48 | 2014 |
Anindya BanerjeeProfessor, IMDEA Software InstituteVerified email at imdea.org
