Josh Berdine

Publication Activity (10 Years)

Years Active: 2002-2023
Publications (10 Years): 4

Top Topics

Spatial Reasoning

Concurrent Programs

Logic Programming

Complete Axiomatization

Top Venues

Proc. ACM Program. Lang.

Publications

Azalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn
A General Approach to Under-Approximate Reasoning About Concurrent Programs. CONCUR (2023)
Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
Concurrent incorrectness separation logic. Proc. ACM Program. Lang. 6 (POPL) (2022)
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. 6 (OOPSLA) (2022)
Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard
Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. CAV (2) (2020)
Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid
Spatial Interpolants. CoRR (2015)
Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid
Spatial Interpolants. ESOP (2015)
Alexey Bakhirkin, Josh Berdine, Nir Piterman
A Forward Analysis for Recurrent Sets. SAS (2015)
Josh Berdine, Nikolaj Bjørner
Computing All Implied Equalities via SMT-Based Partition Refinement. IJCAR (2014)
Alexey Bakhirkin, Josh Berdine, Nir Piterman
Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction. SAS (2014)
Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger
Resourceful Reachability as HORN-LA. LPAR (2013)
Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. Wintersteiger
Diagnosing Abstraction Failure for Separation Logic-Based Analyses. CAV (2012)
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
Verification Condition Generation and Variable Conditions in Smallfoot CoRR (2012)
Josh Berdine, Byron Cook, Samin Ishtiaq
SLAyer: Memory Safety for Systems-Level Code. CAV (2011)
Alexey Gotsman, Josh Berdine, Byron Cook
Precision and the Conjunction Rule in Concurrent Separation Logic. MFPS (2011)
Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine
Structuring the verification of heap-manipulating programs. POPL (2010)
Josh Berdine
Automatic Verification of Heap Manipulation Using Separation Logic. SOFSEM (2009)
M. Ridsdale, Mateja Jamnik, Nick Benton, Josh Berdine
Diagrammatic Reasoning in Separation Logic. Diagrams (2008)
Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine
Heap Decomposition for Concurrent Shape Analysis. SAS (2008)
Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv
Thread Quantification for Concurrent Shape Analysis. CAV (2008)
Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn
Scalable Shape Analysis for Systems Code. CAV (2008)
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv
Local Reasoning for Storable Locks and Threads. APLAS (2007)
Josh Berdine
Local reasoning about storable locks. PPDP (2007)
Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook
Arithmetic Strengthening for Shape Analysis. SAS (2007)
Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv
Shape Analysis by Graph Decomposition. TACAS (2007)
Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv
Thread-modular shape analysis. PLDI (2007)
Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn
Variance analyses from invariance analyses. POPL (2007)
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang
Shape Analysis for Composite Data Structures. CAV (2007)
Alexey Gotsman, Josh Berdine, Byron Cook
Interprocedural Shape Analysis with Separated Heap Abstractions. SAS (2006)
Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn
Automatic Termination Proofs for Programs with Shape-Shifting Heaps. CAV (2006)
Josh Berdine, Peter W. O'Hearn
Strong Update, Disposal, and Encapsulation in Bunched Typing. MFPS (2006)
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
Symbolic Execution with Separation Logic. APLAS (2005)
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
Smallfoot: Modular Automatic Assertion Checking with Separation Logic. FMCO (2005)
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
A Decidable Fragment of Separation Logic. FSTTCS (2004)
Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, Hayo Thielecke
Linear Continuation-Passing. High. Order Symb. Comput. 15 (2-3) (2002)