| Smallfoot: Modular automatic assertion checking with separation logic J Berdine, C Calcagno, PW O’Hearn Formal Methods for Components and Objects, 115-137, 2006 | 487 | 2006 |
| Symbolic execution with separation logic J Berdine, C Calcagno, PW O’Hearn Programming Languages and Systems, 52-68, 2005 | 403 | 2005 |
| Scalable shape analysis for systems code H Yang, O Lee, J Berdine, C Calcagno, B Cook, D Distefano, P O’Hearn International Conference on Computer Aided Verification, 385-398, 2008 | 311 | 2008 |
| Shape analysis for composite data structures J Berdine, C Calcagno, B Cook, D Distefano, PW O'Hearn, T Wies, ... Computer Aided Verification, 178-192, 2007 | 274 | 2007 |
| A decidable fragment of separation logic J Berdine, C Calcagno, PW O’Hearn FSTTCS 2004: Foundations of Software Technology and Theoretical Computer …, 2005 | 252 | 2005 |
| SLAyer: Memory safety for systems-level code J Berdine, B Cook, S Ishtiaq International Conference on Computer Aided Verification, 178-183, 2011 | 152 | 2011 |
| Local reasoning for storable locks and threads A Gotsman, J Berdine, B Cook, N Rinetzky, M Sagiv Asian Symposium on Programming Languages And Systems, 19-37, 2007 | 151 | 2007 |
| Automatic termination proofs for programs with shape-shifting heaps J Berdine, B Cook, D Distefano, P O’Hearn Computer Aided Verification, 386-400, 2006 | 148 | 2006 |
| Interprocedural shape analysis with separated heap abstractions A Gotsman, J Berdine, B Cook International Static Analysis Symposium, 240-260, 2006 | 143 | 2006 |
| Thread-modular shape analysis A Gotsman, J Berdine, B Cook, M Sagiv ACM SIGPLAN Notices 42 (6), 266-277, 2007 | 110 | 2007 |
| Variance analyses from invariance analyses J Berdine, A Chawdhary, B Cook, D Distefano, P O'Hearn Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2007 | 100 | 2007 |
| Arithmetic strengthening for shape analysis S Magill, J Berdine, E Clarke, B Cook International Static Analysis Symposium, 419-436, 2007 | 98 | 2007 |
| Thread quantification for concurrent shape analysis J Berdine, T Lev-Ami, R Manevich, G Ramalingam, M Sagiv International Conference on Computer Aided Verification, 399-413, 2008 | 89 | 2008 |
| 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 | 80 | 2010 |
| Linear continuation-passing J Berdine, P O'Hearn, U Reddy, H Thielecke Higher-Order and Symbolic Computation 15 (2), 181-208, 2002 | 73 | 2002 |
| Heap decomposition for concurrent shape analysis R Manevich, T Lev-Ami, M Sagiv, G Ramalingam, J Berdine International Static Analysis Symposium, 363-377, 2008 | 43 | 2008 |
| Precision and the conjunction rule in concurrent separation logic A Gotsman, J Berdine, B Cook Electronic Notes in Theoretical Computer Science 276, 171-190, 2011 | 31 | 2011 |
| Shape analysis by graph decomposition R Manevich, J Berdine, B Cook, G Ramalingam, M Sagiv International Conference on Tools and Algorithms for the Construction and …, 2007 | 31 | 2007 |
| Spatial interpolants A Albargouthi, J Berdine, B Cook, Z Kincaid European Symposium on Programming Languages and Systems, 634-660, 2015 | 24 | 2015 |
| Linearly used continuations J Berdine, PW O’Hearn, US Reddy, H Thielecke Proceedings of the Third ACM SIGPLAN Workshop on Continuations (CW’01), 47-54, 2000 | 23 | 2000 |
Peter O'HearnFacebook and University College LondonVerified email at ucl.ac.uk
