| Smallfoot: Modular automatic assertion checking with separation logic J Berdine, C Calcagno, PW O’Hearn Formal Methods for Components and Objects, 115-137, 2006 | 517 | 2006 |
| Symbolic execution with separation logic J Berdine, C Calcagno, PW O’Hearn Programming Languages and Systems, 52-68, 2005 | 434 | 2005 |
| Scalable shape analysis for systems code H Yang, O Lee, J Berdine, C Calcagno, B Cook, D Distefano, P O'Hearn CAV 8, 385-398, 2008 | 318 | 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 | 288 | 2007 |
| A decidable fragment of separation logic J Berdine, C Calcagno, PW O’Hearn FSTTCS 2004: Foundations of Software Technology and Theoretical Computer …, 2005 | 278 | 2005 |
| SLAyer: Memory Safety for Systems-Level Code J Berdine, B Cook, S Ishtiaq Computer Aided Verification: 23rd International Conference, CAV 2011 …, 2011 | 171 | 2011 |
| Local reasoning for storable locks and threads A Gotsman, J Berdine, B Cook, N Rinetzky, M Sagiv Programming Languages and Systems: 5th Asian Symposium, APLAS 2007 …, 2007 | 163 | 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 | 150 | 2006 |
| Interprocedural shape analysis with separated heap abstractions A Gotsman, J Berdine, B Cook Static Analysis: 13th International Symposium, SAS 2006, Seoul, Korea …, 2006 | 147 | 2006 |
| Thread-modular shape analysis A Gotsman, J Berdine, B Cook, M Sagiv ACM SIGPLAN Notices 42 (6), 266-277, 2007 | 119 | 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 | 104 | 2007 |
| Arithmetic strengthening for shape analysis S Magill, J Berdine, E Clarke, B Cook Static Analysis: 14th International Symposium, SAS 2007, Kongens Lyngby …, 2007 | 101 | 2007 |
| Thread quantification for concurrent shape analysis J Berdine, T Lev-Ami, R Manevich, G Ramalingam, M Sagiv Computer Aided Verification: 20th International Conference, CAV 2008 …, 2008 | 93 | 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 | 86 | 2010 |
| Linear continuation-passing J Berdine, P O'Hearn, U Reddy, H Thielecke Higher-Order and Symbolic Computation 15 (2), 181-208, 2002 | 74 | 2002 |
| Heap decomposition for concurrent shape analysis R Manevich, T Lev-Ami, M Sagiv, G Ramalingam, J Berdine Lecture Notes in Computer Science 5079, 363-378, 2008 | 43 | 2008 |
| Local reasoning about the presence of bugs: Incorrectness separation logic A Raad, J Berdine, HH Dang, D Dreyer, P O’Hearn, J Villard Computer Aided Verification: 32nd International Conference, CAV 2020, Los …, 2020 | 37 | 2020 |
| 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 | 32 | 2011 |
| Shape analysis by graph decomposition R Manevich, J Berdine, B Cook, G Ramalingam, M Sagiv Tools and Algorithms for the Construction and Analysis of Systems: 13th …, 2007 | 30 | 2007 |
| Spatial interpolants A Albargouthi, J Berdine, B Cook, Z Kincaid Programming Languages and Systems: 24th European Symposium on Programming …, 2015 | 26 | 2015 |
Peter O'HearnLacework and University College LondonVerified email at ucl.ac.uk
