| Smallfoot: Modular automatic assertion checking with separation logic J Berdine, C Calcagno, PW O’Hearn Formal Methods for Components and Objects, 115-137, 2006 | 544 | 2006 |
| Symbolic execution with separation logic J Berdine, C Calcagno, PW O’Hearn Programming Languages and Systems, 52-68, 2005 | 451 | 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 | 330 | 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 | 303 | 2007 |
| A decidable fragment of separation logic J Berdine, C Calcagno, PW O’Hearn FSTTCS 2004: Foundations of Software Technology and Theoretical Computer …, 2005 | 291 | 2005 |
| SLAyer: Memory Safety for Systems-Level Code J Berdine, B Cook, S Ishtiaq Computer Aided Verification: 23rd International Conference, CAV 2011 …, 2011 | 179 | 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 | 167 | 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 | 159 | 2006 |
| Interprocedural shape analysis with separated heap abstractions A Gotsman, J Berdine, B Cook Static Analysis: 13th International Symposium, SAS 2006, Seoul, Korea …, 2006 | 149 | 2006 |
| Thread-modular shape analysis A Gotsman, J Berdine, B Cook, M Sagiv ACM SIGPLAN Notices 42 (6), 266-277, 2007 | 125 | 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 | 111 | 2007 |
| Arithmetic strengthening for shape analysis S Magill, J Berdine, E Clarke, B Cook Static Analysis: 14th International Symposium, SAS 2007, Kongens Lyngby …, 2007 | 104 | 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 | 99 | 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 | 92 | 2010 |
| 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 | 75 | 2020 |
| Linear continuation-passing J Berdine, P O'Hearn, U Reddy, H Thielecke Higher-Order and Symbolic Computation 15 (2), 181-208, 2002 | 72 | 2002 |
| 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 | 56 | 2022 |
| 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 | 46 | 2011 |
| Heap decomposition for concurrent shape analysis R Manevich, T Lev-Ami, M Sagiv, G Ramalingam, J Berdine Static Analysis: 15th International Symposium, SAS 2008, Valencia, Spain …, 2008 | 44 | 2008 |
| 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 | 31 | 2007 |
Peter O'HearnUniversity College LondonVerified email at ucl.ac.uk
