| Smallfoot: Modular automatic assertion checking with separation logic J Berdine, C Calcagno, PW O’Hearn Formal Methods for Components and Objects, 115-137, 2006 | 572 | 2006 |
| Symbolic execution with separation logic J Berdine, C Calcagno, PW O’Hearn Programming Languages and Systems, 52-68, 2005 | 481 | 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 | 334 | 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 | 313 | 2007 |
| A decidable fragment of separation logic J Berdine, C Calcagno, PW O’Hearn FSTTCS 2004: Foundations of Software Technology and Theoretical Computer …, 2005 | 307 | 2005 |
| SLAyer: Memory Safety for Systems-Level Code J Berdine, B Cook, S Ishtiaq International Conference on Computer Aided Verification, 178-183, 2011 | 180 | 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 | 176 | 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 | 162 | 2006 |
| Interprocedural shape analysis with separated heap abstractions A Gotsman, J Berdine, B Cook International Static Analysis Symposium, 240-260, 2006 | 150 | 2006 |
| Thread-modular shape analysis A Gotsman, J Berdine, B Cook, M Sagiv ACM SIGPLAN Notices 42 (6), 266-277, 2007 | 132 | 2007 |
| Local reasoning about the presence of bugs: Incorrectness separation logic A Raad, J Berdine, HH Dang, D Dreyer, P O’Hearn, J Villard International Conference on Computer Aided Verification, 225-252, 2020 | 119 | 2020 |
| 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 | 115 | 2007 |
| Arithmetic strengthening for shape analysis S Magill, J Berdine, E Clarke, B Cook International Static Analysis Symposium, 419-436, 2007 | 105 | 2007 |
| Finding real bugs in big programs with incorrectness logic QL Le, A Raad, J Villard, J Berdine, D Dreyer, PW O'Hearn Proceedings of the ACM on Programming Languages 6 (OOPSLA1), 1-27, 2022 | 103 | 2022 |
| 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 | 101 | 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 | 95 | 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 |
| 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 | 48 | 2011 |
| Heap decomposition for concurrent shape analysis R Manevich, T Lev-Ami, M Sagiv, G Ramalingam, J Berdine International Static Analysis Symposium, 363-377, 2008 | 45 | 2008 |
| Concurrent incorrectness separation logic A Raad, J Berdine, D Dreyer, PW O'Hearn Proceedings of the ACM on Programming Languages 6 (POPL), 1-29, 2022 | 44 | 2022 |
Peter O'HearnUniversity College LondonVerified email at ucl.ac.uk
