Josh Berdine
Josh Berdine
Verified email at fb.com - Homepage
TitleCited byYear
Smallfoot: Modular automatic assertion checking with separation logic
J Berdine, C Calcagno, PW O’Hearn
Formal Methods for Components and Objects, 115-137, 2006
4242006
Symbolic execution with separation logic
J Berdine, C Calcagno, PW O’Hearn
Programming Languages and Systems, 52-68, 2005
3432005
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
2862008
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
2592007
A decidable fragment of separation logic
J Berdine, C Calcagno, PW O’Hearn
FSTTCS 2004: Foundations of Software Technology and Theoretical Computer …, 2005
2162005
Automatic termination proofs for programs with shape-shifting heaps
J Berdine, B Cook, D Distefano, P O’Hearn
Computer Aided Verification, 386-400, 2006
1392006
Interprocedural shape analysis with separated heap abstractions
A Gotsman, J Berdine, B Cook
International Static Analysis Symposium, 240-260, 2006
1362006
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
1352007
SLAyer: Memory safety for systems-level code
J Berdine, B Cook, S Ishtiaq
International Conference on Computer Aided Verification, 178-183, 2011
1302011
Thread-modular shape analysis
A Gotsman, J Berdine, B Cook, M Sagiv
ACM SIGPLAN Notices 42 (6), 266-277, 2007
982007
Variance analyses from invariance analyses
J Berdine, A Chawdhary, B Cook, D Distefano, P O'Hearn
ACM SIGPLAN Notices 42 (1), 211-224, 2007
962007
Arithmetic strengthening for shape analysis
S Magill, J Berdine, E Clarke, B Cook
International Static Analysis Symposium, 419-436, 2007
932007
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
792008
Structuring the verification of heap-manipulating programs
A Nanevski, V Vafeiadis, J Berdine
ACM Sigplan Notices 45 (1), 261-274, 2010
742010
Linear continuation-passing
J Berdine, P O'Hearn, U Reddy, H Thielecke
Higher-Order and Symbolic Computation 15 (2), 181-208, 2002
662002
Heap decomposition for concurrent shape analysis
R Manevich, T Lev-Ami, M Sagiv, G Ramalingam, J Berdine
International Static Analysis Symposium, 363-377, 2008
392008
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
282007
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
242000
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
232011
Spatial interpolants
A Albargouthi, J Berdine, B Cook, Z Kincaid
European Symposium on Programming Languages and Systems, 634-660, 2015
192015
The system can't perform the operation now. Try again later.
Articles 1–20