Josh Berdine

Most-cited papers

Smallfoot: Modular Automatic Assertion Checking with Separation Logic
Josh Berdine, Cristiano Calcagno, P. O'Hearn
2005Formal Methods for Components and Objects426 citations
Semantic Scholar
Symbolic Execution with Separation Logic
Josh Berdine, Cristiano Calcagno, P. O'Hearn
2005Asian Symposium on Programming Languages and Systems373 citations
Semantic Scholar
Scalable Shape Analysis for Systems Code
Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno +3 more
2008International Conference on Computer Aided Verification264 citations
Semantic Scholar
Shape Analysis for Composite Data Structures
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano +3 more
2007International Conference on Computer Aided Verification225 citations Open access
Semantic Scholar
A Decidable Fragment of Separation Logic
Josh Berdine, Cristiano Calcagno, P. O'Hearn
2004Foundations of Software Technology and Theoretical Computer Science224 citations Open access
Semantic Scholar
Local Reasoning for Storable Locks and Threads
Alexey Gotsman, Josh Berdine, B. Cook, N. Rinetzky +1 more
2007Asian Symposium on Programming Languages and Systems143 citations
Semantic Scholar
SLAyer: Memory Safety for Systems-Level Code
Josh Berdine, B. Cook, Samin S. Ishtiaq
2011International Conference on Computer Aided Verification131 citations Open access
Semantic Scholar
Interprocedural Shape Analysis with Separated Heap Abstractions
Alexey Gotsman, Josh Berdine, Byron Cook
2006Sensors Applications Symposium131 citations
Semantic Scholar
Automatic Termination Proofs for Programs with Shape-Shifting Heaps
Josh Berdine, B. Cook, Dino Distefano, P. O'Hearn
2006International Conference on Computer Aided Verification118 citations Open access
Semantic Scholar
Thread-modular shape analysis
Alexey Gotsman, Josh Berdine, Byron Cook, M. Sagiv
2007ACM-SIGPLAN Symposium on Programming Language Design and Implementation107 citations
Semantic Scholar
Variance analyses from invariance analyses
Josh Berdine, A. Chawdhary, B. Cook, Dino Distefano +1 more
2007ACM-SIGACT Symposium on Principles of Programming Languages97 citations
Semantic Scholar
Arithmetic Strengthening for Shape Analysis
S. Magill, Josh Berdine, E. Clarke, B. Cook
2007Sensors Applications Symposium86 citations Open access
Semantic Scholar
Thread Quantification for Concurrent Shape Analysis
Josh Berdine, T. Lev-Ami, R. Manevich, G. Ramalingam +1 more
2008International Conference on Computer Aided Verification84 citations Open access
Semantic Scholar
Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek R. Dreyer +2 more
2020International Conference on Computer Aided Verification82 citations Open access
Semantic Scholar
Finding real bugs in big programs with incorrectness logic
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine +2 more
2022Proc. ACM Program. Lang.79 citations Open access
Semantic Scholar
Structuring the verification of heap-manipulating programs
Aleksandar Nanevski, V. Vafeiadis, Josh Berdine
2010ACM-SIGACT Symposium on Principles of Programming Languages79 citations
Semantic Scholar
Linear Continuation-Passing
Josh Berdine, P. O'Hearn, U. Reddy, Hayo Thielecke
2002High. Order Symb. Comput.60 citations
Semantic Scholar
Heap Decomposition for Concurrent Shape Analysis
R. Manevich, T. Lev-Ami, S. Sagiv, G. Ramalingam +1 more
2008Sensors Applications Symposium34 citations
Semantic Scholar
Concurrent incorrectness separation logic
Azalea Raad, Josh Berdine, Derek R. Dreyer, P. O'Hearn
2022Proc. ACM Program. Lang.29 citations Open access
Semantic Scholar
Precision and the Conjunction Rule in Concurrent Separation Logic
Alexey Gotsman, Josh Berdine, B. Cook
2011Mathematical Foundations of Programming Semantics28 citations Open access
Semantic Scholar
Shape Analysis by Graph Decomposition
R. Manevich, Josh Berdine, B. Cook, G. Ramalingam +1 more
2007International Conference on Tools and Algorithms for Construction and Analysis of Systems23 citations
Semantic Scholar
Spatial Interpolants
Aws Albarghouthi, Josh Berdine, B. Cook, Zachary Kincaid
2015European Symposium on Programming20 citations
Semantic Scholar
Linearly Used Continuations
Josh Berdine, P. O'Hearn, U. Reddy, Hayo Thielecke
200020 citations
Semantic Scholar
Strong Update, Disposal, and Encapsulation in Bunched Typing
Josh Berdine, P. O'Hearn
2006Mathematical Foundations of Programming Semantics15 citations Open access
Semantic Scholar
Modular Automatic Assertion Checking with Separation Logic
Josh Berdine, Cristiano Calcagno, P. O'Hearn
200515 citations
Semantic Scholar
Diagnosing Abstraction Failure for Separation Logic-Based Analyses
Josh Berdine, Arlen Cox, Samin S. Ishtiaq, C. Wintersteiger
2012International Conference on Computer Aided Verification13 citations Open access
Semantic Scholar
Verification, Model Checking, and Abstract Interpretation
R. Giacobazzi, Josh Berdine, Isabella Mastroeni
2013Lecture Notes in Computer Science12 citations Open access
Semantic Scholar
Computing All Implied Equalities via SMT-Based Partition Refinement
Josh Berdine, Nikolaj S. Bjørner
2014International Joint Conference on Automated Reasoning8 citations
Semantic Scholar
A General Approach to Under-Approximate Reasoning About Concurrent Programs
Azalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn
2023International Conference on Concurrency Theory7 citations
Semantic Scholar
Linear and Affine Typing of Continuation-Passing Style
Josh Berdine
20137 citations
Semantic Scholar
A Proposal for Weak-Memory Local Reasoning
Ian Wehrman, Josh Berdine
20117 citations
Semantic Scholar
A Forward Analysis for Recurrent Sets
Alexey Bakhirkin, Josh Berdine, Nir Piterman
2015Sensors Applications Symposium6 citations Open access
Semantic Scholar
Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction
Alexey Bakhirkin, Josh Berdine, Nir Piterman
2014Sensors Applications Symposium6 citations Open access
Semantic Scholar
Resourceful Reachability as HORN-LA
Josh Berdine, Nikolaj S. Bjørner, Samin S. Ishtiaq, J. Kriener +1 more
2013Logic Programming and Automated Reasoning6 citations
Semantic Scholar
Verification Condition Generation and Variable Conditions in Smallfoot
Josh Berdine, Cristiano Calcagno, P. O'Hearn
2012arXiv.org6 citations
Semantic Scholar
Verification, Model Checking, and Abstract Interpretation : 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013, Proceedings
R. Giacobazzi, Josh Berdine, Isabella Mastroeni
20135 citations
Semantic Scholar
Diagrammatic Reasoning in Separation Logic
M. Ridsdale, M. Jamnik, N. Benton, Josh Berdine
2008Diagrams4 citations
Semantic Scholar
Proceedings of the Third ACM SIGPLAN Workshop on Continuations (CW'01)
A. Sabry, C. Talcott, Kwangkeun Yi, Lasse R. Nielsen +4 more
20014 citations
Semantic Scholar
Local reasoning about storable locks
Josh Berdine
2007ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming3 citations
Semantic Scholar
Extracting the Range of cps from Affine Typing
Josh Berdine, Peter W. O'Hearn, Hayo Thielecke
20023 citations
Semantic Scholar
A Forward Analysis for Recurrent Sets Technical Report
Alexey Bakhirkin, Josh Berdine, Nir Piterman
20151 citations
Semantic Scholar
On Affine Typing and Completeness of CPS
Josh Berdine, P. O'Hearn, Hayo Thielecke
20011 citations
Semantic Scholar
Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 7737
R. Giacobazzi, Josh Berdine, Isabella Mastroeni
2013International Conference on Verification, Model Checking and Abstract Interpretation0 citations
Semantic Scholar
Session details: Synthesis & verification
Josh Berdine
2013Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages0 citations
Semantic Scholar
Automatic Verification of Heap Manipulation Using Separation Logic
Josh Berdine
2009Conference on Current Trends in Theory and Practice of Informatics0 citations Open access
Semantic Scholar