Follow
Josh Berdine
Josh Berdine
Verified email at fb.com - Homepage
Title
Cited by
Cited by
Year
Smallfoot: Modular automatic assertion checking with separation logic
J Berdine, C Calcagno, PW O’Hearn
Formal Methods for Components and Objects, 115-137, 2006
5282006
Symbolic execution with separation logic
J Berdine, C Calcagno, PW O’Hearn
Programming Languages and Systems, 52-68, 2005
4402005
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
3192008
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
2922007
A decidable fragment of separation logic
J Berdine, C Calcagno, PW O’Hearn
FSTTCS 2004: Foundations of Software Technology and Theoretical Computer …, 2005
2812005
SLAyer: Memory Safety for Systems-Level Code
J Berdine, B Cook, S Ishtiaq
Computer Aided Verification: 23rd International Conference, CAV 2011 …, 2011
1692011
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
1672007
Automatic termination proofs for programs with shape-shifting heaps
J Berdine, B Cook, D Distefano, P O’Hearn
Computer Aided Verification, 386-400, 2006
1552006
Interprocedural shape analysis with separated heap abstractions
A Gotsman, J Berdine, B Cook
Static Analysis: 13th International Symposium, SAS 2006, Seoul, Korea …, 2006
1482006
Thread-modular shape analysis
A Gotsman, J Berdine, B Cook, M Sagiv
ACM SIGPLAN Notices 42 (6), 266-277, 2007
1232007
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
1052007
Arithmetic strengthening for shape analysis
S Magill, J Berdine, E Clarke, B Cook
Static Analysis: 14th International Symposium, SAS 2007, Kongens Lyngby …, 2007
1022007
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
972008
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
892010
Linear continuation-passing
J Berdine, P O'Hearn, U Reddy, H Thielecke
Higher-Order and Symbolic Computation 15 (2), 181-208, 2002
722002
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
602020
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
442008
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
422011
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
392022
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
312007
The system can't perform the operation now. Try again later.
Articles 1–20