Recent & Upcoming

• VSTTE 2013: Fifth Working Conference on Verified Software: Theories, Tools and Experiments, Atherton, USA, May 17–19, 2013. Program Committee member.
• PLOOC 2013: 1st Workshop on Programming Languages Technology for Massive Open Online Courses, Seattle, Washington, USA, June 21, 2013 (co-located with PLDI 2013). Program Committee member.

Publications

(DBLP) (MS Academic) (Google Scholar)

• Diagnosing Abstraction Failure for Separation Logic–based Analyses.
  Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. Wintersteiger.
  In CAV 2012.
• SLAyer: Memory Safety for Systems-level Code.
  Josh Berdine, Byron Cook, Samin Ishtiaq.
  In CAV 2011.
• A Proposal for Weak-Memory Local Reasoning.
  Ian Wehrman, Josh Berdine.
  In LOLA 2011.
• Precision and the Conjunction Rule in Concurrent Separation Logic.
  Alexey Gotsman, Josh Berdine, Byron Cook.
  In MFPS 2011.
• Structuring the Verification of Heap-Manipulating Programs.
  Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.
  In POPL 2010. (Coq scripts) (ACM DL)
• 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. (Extended version) (ACM DL)
• 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. (ACM DL)
• 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. (ACM DL)
• 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.
• Verification Condition Generation and Variable Conditions in Smallfoot.
  Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn.
  Draft 2005. Introduction updated 2012.
• 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

• SSV 09: The 4th International Workshop on
  Systems Software Verification, June 22–24, 2009, Aachen, Germany.
• APV: The Symposium on Automatic Program Verification, Río Cuarto, Argentina, February 15, 2009.
• 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.
• 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

• POPL 2013: The 40th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Rome, Italy, January 23–25, 2013. Program Committee member.
• VMCAI 2013: The14th International symposium on Verification, Model Checking and Abstract Interpretation, Rome, Italy, January 20–22, 2013. Program Committee co-chair.
• POPL 2012: The 39th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Philadelphia, USA, January 25–27, 2012. External Review Committee member.
• VMCAI 2012: The 13th International Conference on Verification, Model Checking, and Abstract Interpretation, Philadelphia, USA, January 22–24, 2012 (co-located with POPL 2012). Program Committee member.
• ICFP 2011: The 16th ACM SIGPLAN International Conference on Functional Programming, September 19–21, 2011, Tokyo, Japan. Program Committee member.
• FMICS 2011: The 16th International Workshop on Formal Methods for Industrial Critical Systems, Trento, Italy, August 29–30, 2011. Program Committee member.
• LOLA 2011: Syntax and Semantics of Low-Level Languages. June 20, 2011, Toronto, Canada. (A satellite workshop of Logic in Computer Science, LICS 2011) Program Committee member.
• FASE 2011: The 14th International Conference on Fundamental Approaches to Software Engineering, A member conference of the European Joint Conferences on Theory and Practice of Software (ETAPS 2011), March 26–April 4, 2011, Saarbrucken, Germany. Program Committee member.
• VMCAI 2011: The 12th International Conference on Verification, Model Checking, and Abstract Interpretation, January 23–25, 2011, Austin, Texas, USA (co-located with POPL 2011). 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.
• FMICS 2009: The 14th International Workshop on Formal Methods for Industrial Critical Systems, Eindhoven, The Netherlands, November 2–3, 2009. Program Committee member.
• CSR 2009: The 4th International Computer Science Symposium in Russia, August 18–23, 2009, Novosibirsk, Russia. Program Committee member, Application Track.
• 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 (co-located 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