Recent & Upcoming

• Invited talk at SOFSEM 09: The 35th International Conference on Current Trends in Theory and Practice of Computer Science, January 24–30, 2009, Špindlerův Mlýn, Czech Republic.
• Keynote talk at APV: The Symposium on Automatic Program Verification, Río Cuarto, Argentina, February 15, 2009.
• Invited talk at SSV 09: The 4th International Workshop on
  Systems Software Verification, June 22–24, 2009, Aachen, Germany.
• CSR 2009: The 4th International Computer Science Symposium in Russia, August 18–23, 2009, Novosibirsk, Russia.  Program Committee member, Application Track. (call for papers)
• FMICS 2009: The 14th International Workshop on Formal Methods for Industrial Critical Systems, Eindhoven, The Netherlands, November 2–3, 2009. Program Committee member.
• TACAS 2010: The 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, A member conference of the European Joint Conferences on Theory and Practice of Software (ETAPS 2010), March 20–28, 2010, Paphos, Cyprus. Program Committee member.

Publications

(BiBTeX) (DBLP)

• Scalable Shape Analysis for Systems Code.
  Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter O'Hearn.
  In CAV 2008.
• Thread Quantification for Concurrent Shape Analysis.
  Josh Berdine, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, and Mooly Sagiv.
  In CAV 2008.
• Heap Decomposition for Concurrent Shape Analysis.
  Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, and Josh Berdine.
  In SAS 2008.
• Local Reasoning for Storable Locks and Threads.
  Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv.
  In APLAS 2007.
• Arithmetic Strengthening for Shape Analysis.
  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.
• 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 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.
  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.
  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.

Invited Talks

• 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.

Program Committees

• 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.
• 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.

Contact