About Me


I'm a researcher at Samsung Research America, Silicon Valley, the new Frontier Computer Science Lab.

I am interested in finding new ways to improve software reliability, especially providing strong static guarantees about program behavior, for 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.

Contact

  • Work email: colin.gordon@samsung.com
  • Personal email: csgordon@cs.washington.edu or colin.s.gordon@gmail.com

News

  • 7/2/14: I have successfully defended my PhD.
  • 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.

Publications


Partial publication lists are also available on Google Scholar, the ACM portal, and DBLP. I'm gradually locating older slide decks including non-conference talks and putting them up on SpeakerDeck.

In Submission

  • Concurrent Refinement Types via Rely-Guarantee References
    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 2013), Montpellier, France. July 2013
    Colin S. Gordon, Werner M. Dietl, Michael D. Ernst, and Dan Grossman
    Acceptance Rate 25% (29/116)
    [+abstract] [ springer | pdf | tech report ] [ slides ] [ code ] [ code at submission + subject programs ]
  • 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 2013), Seattle, WA, USA. June 2013
    Colin S. Gordon, Michael D. Ernst, and Dan Grossman
    Acceptance Rate 17% (46/267)
    [+abstract] [ acm authorizer | acm | 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 2012), Tucson, AZ, USA. October 2012
    Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy
    Acceptance Rate 26% (59/228)
    [+abstract] [ acm authorizer | pdf | tech report ]

Workshop Papers

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

Theses

  • Verifying Concurrent Programs by Controlling Alias Interference
    University of Washington PhD Dissertation, Seattle, WA, USA. August 2014
    Colin S. Gordon
    [+abstract] [ pdf ] [ entry @ UW ResearchWorks Archive ]
  • Type-Safe Stack Traversal for Garbage Collector Implementation
    Brown University Senior Honors Thesis, Providence, RI, USA. May 2008
    Colin Stebbins Gordon
    [+abstract] [ pdf ] [ other honors theses ]

Technical Reports

  • 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] [ pdf ] [ dept pdf ]
  • 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] [ pdf ] [ dept pdf ]
  • 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] [ pdf ] [ dept pdf ]
  • 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] [ department page | pdf ]

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