Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Josh Berdine

Projects

I am a member of the Programming Principles and Tools group and lead the Verification and Automatic Reasoning Group.

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

Josh Berdine
RESEARCHER
.

Recent & Upcoming

  • PLACES 15: Programming Language Approaches to Communication- and Concurrency-cEntric Systems(workshop affiliated with ETAPS 2015), London, United Kingdom, April 18, 2015. Program Committee member.
  • CADE-25: The 25th International Conference on Automated Deduction, Berlin, Germany, August 2–7, 2015. Program Committee member.
  • SAS 2015: The 22nd International Static Analysis Symposium, Saint-Malo, France, September 9–11, 2015. Program Committee member.

Publications

(DBLP) (MS Academic) (Google Scholar)

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 2015: The 42nd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Mumbai, India, January 11–18, 2015. External Review Committee member.
  • LPAR-19: 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Stellenbosch, South Africa, December 15-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.
  • VSTTE 2013: Fifth Working Conference on Verified Software: Theories, Tools and Experiments, Atherton, USA, May 17–19, 2013. Program Committee member.
  • 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

jjb@microsoft.com

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

Microsoft Research Limited
21 Station Road
Cambridge CB1 2FB
United Kingdom