I'm a researcher in the Programming Principles and Tools Group. I have been a member of the East London Massive since its inception.

Most of my time is spent working on SLAyer, a formal verification tool aimed at ensuring correct use of dynamically-allocated heap memory. I'm also involved in the TERMINATOR project, where termination and other liveness properties are proved. Before joining MSR, I worked on Smallfoot, an automatic specification checking tool focused on the heap. I also talk to the SpaceInvader guys all the time.

• LPAR 2008: 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, November 22-27, 2008, Doha, Qatar. Program committee member.
  
  
• HAV 2008: Heap Analysis and Verification workshop (affiliated with CAV'08), July 14, 2008, Princeton, New Jersey. Co-organizer with Mooly Sagiv and Eran Yahav.
  
  
• SPACE 2009: Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (to be colocated with POPL 2009), January 21--23 2009, Savannah Georgia, USA. Program committee member.
  
  

• Scalable Shape Analysis for Systems Code.
  Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter O'Hearn.
  To appear in CAV 2008.
  
  
• Thread Quantification for Concurrent Shape Analysis.
  Josh Berdine, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, and Mooly Sagiv.
  To appear in CAV 2008.
  
  
• Heap Decomposition for Concurrent Shape Analysis.
  Roman Manevich, Tal Lev-Ami, Ganesan Ramalingam, Mooly Sagiv, and Josh Berdine.
  To appear in SAS 2008. Also Tel Aviv University School of Computer Science Technical Report TR-2007-11-85453.
  
  
• Local Reasoning for Storable Locks and Threads.
  Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv.
  In APLAS 2007. Also Microsoft Research Technical Report MSR-TR-2007-39.
  Slides from my invited PPDP talk on this material.
  
  
• Arithmetic Strengthening of Shape Analyses Based On Separation Logic.
  Stephen Magill, Josh Berdine, Edmund Clarke, and Byron Cook.
  In SAS 2007.
  
  
• Shape Analysis for Composite Data Structures.
  Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, and Hongseok Yang.
  In CAV 2007. Also Microsoft Research Technical Report MSR-TR-2007-13.
  
  
• Thread-Modular Shape Analysis.
  Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv.
  In PLDI 2007.
  
  
• Shape Analysis by Graph Decomposition.
  Roman Manevich, Josh Berdine, Byron Cook, Ganesan Ramalingam, and Mooly Sagiv.
  In TACAS 2007.
  
  
• Variance Analyses from Invariance Analyses.
  Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano and Peter W. O'Hearn.
  In POPL 2007.
  
  
• Interprocedural Shape Analysis with Separated Heap Abstractions.
  Alexey Gotsman, Josh Berdine, and Byron Cook.
  In SAS 2006.
  
  
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps.
  Josh Berdine, Byron Cook, Dino Distefano, and Peter W. O'Hearn.
  In CAV 2006.
  
  
• Strong Update, Disposal, and Encapsulation in Bunched Typing.
  Josh Berdine and Peter W. O'Hearn.
  In MFPS 2006.
  
  
• Smallfoot: Modular Automatic Assertion Checking with Separation Logic.
  Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn.
  In FMCO 2005.
  
  
• Symbolic Execution with Separation Logic. (preprint)
  Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn.
  In APLAS 2005.
  
  
• A Decidable Fragment of Separation Logic.
  Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn.
  In FSTTCS 2004.
  
  
• Linear and Affine Typing of Continuation-Passing Style. (booklet, official)
  Joshua James Berdine.
  PhD thesis, Queen Mary, University of London, London, United Kingdom, 2004.
  Examined by Olivier Danvy and Michael Huth.
  
  
• Extracting the Range of CPS from Affine Typing: Extended Abstract.
  Josh Berdine, Peter O'Hearn, and Hayo Thielecke.
  Presented at FLoC'02 Workshop on Linear Logic (LL 2002).
  
  
• Linear Continuation-Passing.
  Josh Berdine, Peter O'Hearn, Uday S. Reddy, and Hayo Thielecke.
  Higher-Order and Symbolic Computation, 15(2/3):181-208, 2002.
  
  
• Linearly Used Continuations.
  Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, and Hayo Thielecke. In CW'01. Superseded by Linear Continuation-Passing.

• PPDP 2007: 9th International Symposium on Principles and Practice of Declarative Programming (colocated with ICALP 2007, LICS 2007, and LC 2007), 14-16 July 2007, Wroclaw, Poland.
  
  
• SAVCBS'06: Specification and Verification of Component-Based Systems (workshop at ACM SIGSOFT 2006/FSE-14), November 10-11 2006, Portland Oregon, USA.

• PPDP 2007: 9th International Symposium on Principles and Practice of Declarative Programming (colocated with ICALP 2007, LICS 2007, and LC 2007), 14-16 July 2007, Wroclaw, Poland. Program Committee member.
  
  
• HAV 2007: Heap Analysis and Verification workshop (a satellite of ETAPS 2007), 25 March 2007, Braga, Portugal. Co-organizer with Mooly Sagiv.

jjb@microsoft.com

Microsoft Research Limited
Roger Needham Building
7 J J Thomson Avenue
Cambridge CB3 0FB
United Kingdom

Tel: +44 1223 479775
Fax: +44 1223 479999