About Me


I've just finished my PhD at the University of Washington, and am now a researcher at Samsung Research America.

I am interested in finding new ways to improve software reliability, especially providing strong static guarantees about program behavior, with a particular interest in concurrent and systems-level code. My work has focused on formal verification of concurrent programs, though I'm also interested in new other levels of formal assurance, programming models, distributed computing, and even testing.

I completed my PhD (2014) and MS (2011) at the University of Washington, focusing on formal verification of concurrent programs, co-advised by Michael Ernst and Dan Grossman, with a lot of input from Matt Parkinson. I earned my ScB from Brown University in 2008, where I worked with Shriram Krishnamurthi and Maurice Herlihy. I've interned with NetApp's filesystem group, the Solaris kernel group at Sun pre-Oracle, and have been both a full-time employee (before grad school) and intern (during grad school) with an operating system incubation group at Microsoft.

News

  • 6/2/14: This summer I'll be joining Samsung Research America as a researcher in their new programming languages and software engineering group.
  • 4/14: The GUI Effect Checker from my JavaUI paper (ECOOP'13) is now part of the Checker Framework.
  • 2/14: I will be on the PC for IWACO 2014, affiliated with ECOOP 2014.
  • 11/13: I have posted my job application packet.
  • 9/26/13: I'm now the proud father of Henry Ryan Gordon!
  • 5/20/13: I will be giving an invited talk at Languages for the Multicore Era (LaME) 2013.
  • 3/4/13: "JavaUI: Effects for Controlling UI Object Access" will appear at ECOOP'13.
  • 2/4/13: "Rely-Guarantee References for Refinement Types over Aliased Mutable Data" will appear at PLDI'13.

Publications


Partial publication lists are also available on Google Scholar, the ACM portal, and DBLP.

In Preparation

  • Towards Heaps in Dependent Type Theory.
    Colin S. Gordon.
    [+abstract]

In Submission

  • Rely-Guarantee References for Lock-Free Data Structures.
    Colin S. Gordon, Michael D. Ernst, Dan Grossman, and Matt Parkinson.
    [+abstract] [code]

Conference Papers

  • JavaUI: Effects for Controlling UI Object Access.
    In Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP'13), Montpellier, France. July 2013.
    Colin S. Gordon, Werner M. Dietl, Michael D. Ernst, and Dan Grossman.
    Acceptance rate 25% (29/116).
    [+abstract] [+bibtex] [ springer | pdf | tech report] [slides] [new code] [old code]
    This project has now been incorporated into the Checker Framework.
  • Rely-Guarantee References for Refinement Types over Aliased Mutable Data.
    In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'13), Seattle, WA, USA. June 2013.
    Colin S. Gordon, Michael D. Ernst, and Dan Grossman.
    Acceptance rate 17% (46/267).
    [+abstract] [+bibtex] [acm | acm authorizer | pdf | tech report] [slides] [code]
  • Uniqueness and Reference Immutability for Safe Parallelism.
    In Proceedings of the 27th ACM SIGPLAN Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA'12), Tucson, AZ, USA. October 2012.
    Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy.
    Acceptance rate 26% (59/228).
    [+abstract] [+bibtex] [acm | acm authorizer | pdf | tech report | tech report @ msr ] [slides]
    [Press: slashdot | reddit | hacker news (most coverage misunderstood the work)]

Workshop Papers

  • Static Lock Capabilities for Deadlock Freedom.
    In Proceedings of the 8th Workshop on Types in Language Design and Implementation (TLDI'12), Philadelphia, PA, USA. January 2012.
    Colin S. Gordon, Michael D. Ernst, and Dan Grossman.
    [+abstract] [+bibtex] [acm | acm authorizer | pdf | tech report] [slides] [conference homepage]
  • Formal Semantics for Testing.
    In Off the Beaten Track Workshop (OBT'12), Philadelphia, PA, USA. January 2012. Position paper.
    Colin S. Gordon.
    [+abstract] [+bibtex] [pdf] [slides] [conference homepage | schedule]
  • Composition with Consistent Updates for Abstract State Machines.
    In Proceedings of the 14th International Workshop on Abstract State Machines (ASM'07), Grimstad, Norway. June 2007.
    Colin Gordon, Leo Meyerovich, Joel Weinberger, and Shriram Krishnamurthi.
    [+abstract] [+bibtex] [pdf] [proceedings]

Theses and Technical Reports

  • Verifying Concurrent Programs by Controlling Alias Interference.
    PhD Dissertation. University of Washington, 2014.
    Colin S. Gordon.
    [+abstract] [pdf]
  • JavaUI: Effects for Controlling UI Object Access (Extended Version).
    Technical Report UW-CSE-13-04-01, Computer Science and Engineering, University of Washington, Seattle, WA, USA. April 2013.
    Colin S. Gordon, Werner M. Dietl, Michael D. Ernst, and Dan Grossman.
    [+abstract] [+bibtex] [ dept pdf | dept TRs] [code]
  • Rely-Guarantee References for Refinement Types Over Aliased Mutable Data (Extended Version).
    Technical Report UW-CSE-13-03-02, Computer Science and Engineering, University of Washington, Seattle, WA, USA. March 2013.
    Colin S. Gordon, Michael D. Ernst, Dan Grossman.
    [+abstract] [+bibtex] [pdf ] [dept pdf | dept TRs]
  • Uniqueness and Reference Immutability for Safe Parallelism (Extended Version).
    Technical Report MSR-TR-2012-79, Microsoft Research, Redmond, WA, USA. August 2012.
    Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy.
    [+abstract] [ pdf | pdf @ msr ]
  • Static Lock Capabilities for Deadlock Freedom.
    Technical Report UW-CSE-11-10-01, Computer Science and Engineering, University of Washington, Seattle, WA, USA. October 2011.
    Colin S. Gordon, Michael D. Ernst, Dan Grossman.
    [+abstract] [+bibtex] [pdf ] [dept pdf | dept TRs]
  • Type-Safe Stack Traversal for Garbage Collector Implementation.
    Brown University Senior Honors Thesis. May 2008. Undergraduate Thesis.
    Colin Stebbins Gordon.
    [+abstract] [+bibtex] [pdf] [slides] [other honors theses]
  • ASM Relational Transducer Security Policies.
    Technical Report CS-06-12, Computer Science Department, Brown University, Providence, RI, USA. November, 2006.
    Meyerovich, L.A., Weinberger, J.H.W., Gordon, C.S., Krishnamurthi, S.
    [+abstract] [+bibtex] [pdf ] [department page]
    This report is essentially an extended version of Composition with Consistent Updates for Abstract State Machines

Patents

  • Merging Containers in a Multi-Container System.
    US Patent 7828201. Filed April, 2007, issued November 2010. Assigned to Network Appliance.
    Colin Stebbins Gordon, Pratap Vikram Singh, and Donald Alvin Trimmer.
    [ Patent at USPTO ]
  • Data Containerization for Reducing Unused Space in a File System.
    US Patent 7739312. Filed April, 2007, issued June 2010. Assigned to Network Appliance.
    Colin Stebbins Gordon, Pratap Vikram Singh, and Donald Alvin Trimmer.
    [ Patent at USPTO ]

Service


Industry Experience


  • Microsoft: Technical Strategy Incubation - Intern, Program analysis work. See OOPSLA'12 publication. (Summer 2011)
  • Microsoft: Technical Strategy Incubation - Full Time, Kernel developer on an unannounced systems project. Worked on kernel debugger implementation, interrupt handling, post-mortem debugging, platform abstractions, all work interacting with other subsystems. (August 2008 - September 2009)
  • Sun Microsystems: Solaris Kernel Group - Intern, merged two processor grouping scheduler abstractions. (Summer 2007)
  • NetApp: Filesystems Group - Intern, designed, documented, and implemented special-purpose filesystem. Resulted in two patents, listed above. (Summer 2006)

Honors


Teaching


Interesting Readings