Josh Berdine

Roberto Giacobazzi, Josh Berdine, Isabella Mastroeni (Eds.): Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings. Lecture Notes in Computer Science 7737, Springer 2013, isbn 978-3-642-35872-2

Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. Wintersteiger: Diagnosing Abstraction Failure for Separation Logic-Based Analyses. CAV 2012: 155-173

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn: Verification Condition Generation and Variable Conditions in Smallfoot. CoRR abs/1204.4804 (2012)

Alexey Gotsman, Josh Berdine, Byron Cook: Precision and the Conjunction Rule in Concurrent Separation Logic. Electr. Notes Theor. Comput. Sci. 276: 171-190 (2011)

Josh Berdine, Byron Cook, Samin Ishtiaq: SLAyer: Memory Safety for Systems-Level Code. CAV 2011: 178-183

Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine: Structuring the verification of heap-manipulating programs. POPL 2010: 261-274

Josh Berdine: Automatic Verification of Heap Manipulation Using Separation Logic. SOFSEM 2009: 34

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

Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv: Thread Quantification for Concurrent Shape Analysis. CAV 2008: 399-413

M. Ridsdale, Mateja Jamnik, Nick Benton, Josh Berdine: Diagrammatic Reasoning in Separation Logic. Diagrams 2008: 408-411

Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine: Heap Decomposition for Concurrent Shape Analysis. SAS 2008: 363-377

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv: Local Reasoning for Storable Locks and Threads. APLAS 2007: 19-37

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

Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv: Thread-modular shape analysis. PLDI 2007: 266-277

Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn: Variance analyses from invariance analyses. POPL 2007: 211-224

Josh Berdine: Local reasoning about storable locks. PPDP 2007: 153

Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook: Arithmetic Strengthening for Shape Analysis. SAS 2007: 419-436

Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv: Shape Analysis by Graph Decomposition. TACAS 2007: 3-18

Josh Berdine, Peter W. O'Hearn: Strong Update, Disposal, and Encapsulation in Bunched Typing. Electr. Notes Theor. Comput. Sci. 158: 81-98 (2006)

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

Alexey Gotsman, Josh Berdine, Byron Cook: Interprocedural Shape Analysis with Separated Heap Abstractions. SAS 2006: 240-260

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn: Symbolic Execution with Separation Logic. APLAS 2005: 52-68

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

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn: A Decidable Fragment of Separation Logic. FSTTCS 2004: 97-109

Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, Hayo Thielecke: Linear Continuation-Passing. Higher-Order and Symbolic Computation 15(2-3): 181-208 (2002)