Smallfoot: Modular automatic assertion checking with separation logic J Berdine, C Calcagno, PW O’hearn Formal Methods for Components and Objects, 115-137 | 286 | | 2006 |

Symbolic execution with separation logic J Berdine, C Calcagno, PW O’hearn Programming Languages and Systems, 52-68 | 213 | | 2005 |

Scalable shape analysis for systems code H Yang, O Lee, J Berdine, C Calcagno, B Cook, D Distefano, P O’Hearn Computer Aided Verification, 385-398 | 204 | | 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 | 196 | | 2007 |

A decidable fragment of separation logic J Berdine, C Calcagno, PW O’hearn FSTTCS 2004: Foundations of Software Technology and Theoretical Computer ... | 135 | | 2005 |

Interprocedural shape analysis with separated heap abstractions A Gotsman, J Berdine, B Cook Static Analysis, 240-260 | 113 | | 2006 |

Local reasoning for storable locks and threads A Gotsman, J Berdine, B Cook, N Rinetzky, M Sagiv Programming Languages and Systems, 19-37 | 110 | | 2007 |

Automatic termination proofs for programs with shape-shifting heaps J Berdine, B Cook, D Distefano, P O’Hearn Computer Aided Verification, 386-400 | 105 | | 2006 |

Arithmetic strengthening for shape analysis S Magill, J Berdine, E Clarke, B Cook Static Analysis, 419-436 | 79 | | 2007 |

Variance analyses from invariance analyses J Berdine, A Chawdhary, B Cook, D Distefano, P O'Hearn ACM SIGPLAN Notices 42 (1), 211-224 | 74 | | 2007 |

Thread-modular shape analysis A Gotsman, J Berdine, B Cook, M Sagiv ACM SIGPLAN Notices 42 (6), 266-277 | 71 | | 2007 |

SLAyer: Memory safety for systems-level code J Berdine, B Cook, S Ishtiaq Computer Aided Verification, 178-183 | 54 | | 2011 |

Linear continuation-passing J Berdine, P O'Hearn, U Reddy, H Thielecke Higher-Order and Symbolic Computation 15 (2), 181-208 | 53 | | 2002 |

Thread quantification for concurrent shape analysis J Berdine, T Lev-Ami, R Manevich, G Ramalingam, M Sagiv Computer Aided Verification, 399-413 | 51 | | 2008 |

Structuring the verification of heap-manipulating programs A Nanevski, V Vafeiadis, J Berdine ACM Sigplan Notices 45 (1), 261-274 | 43 | | 2010 |

Heap decomposition for concurrent shape analysis R Manevich, T Lev-Ami, M Sagiv, G Ramalingam, J Berdine Static Analysis, 363-377 | 30 | | 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, 3-18 | 25 | | 2007 |

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 | 22 | | 2000 |

Precision and the conjunction rule in concurrent separation logic A Gotsman, J Berdine, B Cook Electronic Notes in Theoretical Computer Science 276, 171-190 | 15 | | 2011 |

Strong update, disposal, and encapsulation in bunched typing J Berdine, PW O'Hearn Electronic Notes in Theoretical Computer Science 158, 81-98 | 13 | | 2006 |