Linear Continuation-Passing. - Josh Berdine; Peter W. O'Hearn; Uday S. Reddy; Hayo Thielecke (High. Order Symb. Comput., 2002)

A Decidable Fragment of Separation Logic. - Josh Berdine; Cristiano Calcagno; Peter W. O'Hearn (FSTTCS, 2004)

Symbolic Execution with Separation Logic. - Josh Berdine; Cristiano Calcagno; Peter W. O'Hearn (APLAS, 2005)

Smallfoot: Modular Automatic Assertion Checking with Separation Logic. - Josh Berdine; Cristiano Calcagno; Peter W. O'Hearn (FMCO, 2005)

Automatic Termination Proofs for Programs with Shape-Shifting Heaps. - Josh Berdine; Byron Cook; Dino Distefano; Peter W. O'Hearn (CAV, 2006)

Interprocedural Shape Analysis with Separated Heap Abstractions. - Alexey Gotsman; Josh Berdine; Byron Cook (SAS, 2006)

Strong Update, Disposal, and Encapsulation in Bunched Typing. - Josh Berdine; Peter W. O'Hearn (MFPS, 2006)

Local Reasoning for Storable Locks and Threads. - Alexey Gotsman; Josh Berdine; Byron Cook; Noam Rinetzky; Mooly Sagiv (APLAS, 2007)

Shape Analysis for Composite Data Structures. - Josh Berdine; Cristiano Calcagno; Byron Cook; Dino Distefano; Peter W. O'Hearn; Thomas Wies; Hongseok Yang (CAV, 2007)

Thread-modular shape analysis. - Alexey Gotsman; Josh Berdine; Byron Cook; Mooly Sagiv (PLDI, 2007)

Variance analyses from invariance analyses. - Josh Berdine; Aziem Chawdhary; Byron Cook; Dino Distefano; Peter W. O'Hearn (POPL, 2007)

Local reasoning about storable locks. - Josh Berdine (PPDP, 2007)

Arithmetic Strengthening for Shape Analysis. - Stephen Magill; Josh Berdine; Edmund M. Clarke; Byron Cook (SAS, 2007)

Shape Analysis by Graph Decomposition. - Roman Manevich; Josh Berdine; Byron Cook; G. Ramalingam; Mooly Sagiv (TACAS, 2007)

Thread Quantification for Concurrent Shape Analysis. - Josh Berdine; Tal Lev-Ami; Roman Manevich; G. Ramalingam; Shmuel Sagiv (CAV, 2008)

Scalable Shape Analysis for Systems Code. - Hongseok Yang; Oukseh Lee; Josh Berdine; Cristiano Calcagno; Byron Cook; Dino Distefano; Peter W. O'Hearn (CAV, 2008)

Diagrammatic Reasoning in Separation Logic. - M. Ridsdale; Mateja Jamnik; Nick Benton; Josh Berdine (Diagrams, 2008)

Heap Decomposition for Concurrent Shape Analysis. - Roman Manevich; Tal Lev-Ami; Mooly Sagiv; Ganesan Ramalingam; Josh Berdine (SAS, 2008)

Automatic Verification of Heap Manipulation Using Separation Logic. - Josh Berdine (SOFSEM, 2009)

Structuring the verification of heap-manipulating programs. - Aleksandar Nanevski; Viktor Vafeiadis; Josh Berdine (POPL, 2010)

SLAyer: Memory Safety for Systems-Level Code. - Josh Berdine; Byron Cook; Samin Ishtiaq (CAV, 2011)

Precision and the Conjunction Rule in Concurrent Separation Logic. - Alexey Gotsman; Josh Berdine; Byron Cook (MFPS, 2011)

Diagnosing Abstraction Failure for Separation Logic-Based Analyses. - Josh Berdine; Arlen Cox; Samin Ishtiaq; Christoph M. Wintersteiger (CAV, 2012)

Verification Condition Generation and Variable Conditions in Smallfoot - Josh Berdine; Cristiano Calcagno; Peter W. O'Hearn (CoRR, 2012)

Resourceful Reachability as HORN-LA. - Josh Berdine; Nikolaj S. Bjørner; Samin Ishtiaq; Jael E. Kriener; Christoph M. Wintersteiger (LPAR, 2013)

Computing All Implied Equalities via SMT-Based Partition Refinement. - Josh Berdine; Nikolaj S. Bjørner (IJCAR, 2014)

Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction. - Alexey Bakhirkin; Josh Berdine; Nir Piterman (SAS, 2014)

Spatial Interpolants. - Aws Albarghouthi; Josh Berdine; Byron Cook; Zachary Kincaid (ESOP, 2015)

A Forward Analysis for Recurrent Sets. - Alexey Bakhirkin; Josh Berdine; Nir Piterman (SAS, 2015)

Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. - Azalea Raad; Josh Berdine; Hoang-Hai Dang; Derek Dreyer; Peter W. O'Hearn; Jules Villard (CAV (2), 2020)

Finding real bugs in big programs with incorrectness logic. - Quang Loc Le; Azalea Raad; Jules Villard; Josh Berdine; Derek Dreyer; Peter W. O'Hearn (Proc. ACM Program. Lang., 2022)

Concurrent incorrectness separation logic. - Azalea Raad; Josh Berdine; Derek Dreyer; Peter W. O'Hearn (Proc. ACM Program. Lang., 2022)

A General Approach to Under-Approximate Reasoning About Concurrent Programs. - Azalea Raad; Julien Vanegue; Josh Berdine; Peter W. O'Hearn (CONCUR, 2023)