About Me

I am an Assistant Professor in the Computer Science Department of Drexel University's College of Computing and Informatics. 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 using static reference capabilities and effect systems, though I'm also interested in other levels of formal assurance, programming models, distributed computing, and even testing. Right now I'm working on theory and application of type systems for JavaScript, polymorphic effect systems, verification for operating systems kernels, and tools to connect natural language to machine language (code and formal specifications). See my publications page for more details.

Contact

• Email: csgordon@cs.drexel.edu
• Office: University Crossings, Room 100G

News

• 6/20: I'll be on the PC for OOPSLA 2021, which will have a late spring 2021 deadline (I'll update this with links when available)
• 6/20: My NSF proposal to work on Making Effect Systems Practical with Polymorphism, Inference, and Prototyping Support has been funded! I'm looking for PhD students and undergraduate research co-op students for this!
• 5/20: I'll be on the PC for AGERE 2020, which will be held (virtually or physically) with SPLASH and OOPSLA 2020, possibly in Chicago, IL. Please submit your interesting work on actors, agents, and related concurrency issues by September 1!
• 5/20: I'll be on the PC for ECOOP 2021, which will be held in Aarhus, Denmark. Please submit some of your best work by January 11, 2021!
• 4/20: I'm thrilled to have two papers appearing in ECOOP 2020:
  • Designing with Static Capabilities and Effects
  • Lifting Sequential Effects to Control Operators
• 1/20: I'm teaching SE576: Software Reliability and Testing this term
• 9/19: I'll be presenting my paper Modal Assertions for Actor Corrrectness at AGERE 2019 in October!
• 9/19: This term I'm teaching SE320 Software Verification and Validation
• 4/19: This term I'm teaching CS647 Distributed Systems
• 2/19: It's official: My NSF CAREER award, Modal Abstractions of Systems Concepts for OS Kernel Verification, has been funded!
• 1/19: Congratulations to my student Ismail Kuru, whose paper "Safe Deferred Memory Reclamation with Types" was accepted to ESOP 2019!
• 1/19: I'm teaching SE576: Software Reliability and Testing this term
• 12/18: I'm co-chairing the OOPSLA 2019 Artifact Evaluation Committee along with Jan Vitek
• 11/18: I'm on the PC for POPL 2020. The deadline will be mid-2019; please consider submitting!
• 11/18: I'm honored to have been given a Distinguished Reviewer Award for my work on the OOPSLA 2018 PC! The other Distinguished Reviewer was Derek Dreyer
• 10/18: NL4SE (collocated with FSE 2018) has accepted an early results paper with my student Sergey Matskevich, Generating Comments from Source Code with CCGs. Sergey will be giving the talk.
• 8/18: I'll be giving a talk at OCAP 2018 about the trade-offs between static capability systems and effect systems, collocated with OOPSLA 2018
• 12/17: I'll be speaking about Synthesizing Program-Specific Static Analyses and the 2018 Off the Beaten Track Workshop, collocated with POPL 2018!
• 7/17: I'm on the OOPSLA 2018 Program Committee. Submit! The deadline is April 16, 2018.
• 6/17: The videos of my talks from Barcelona are online, linked from my Publications page and from the individual pages for my ECOOP 2017 paper and my TOPLAS 2017 paper (which was presented at PLDI 2017).
• 4/17: April has been busy:
  • My paper A Generic Approach to Flow-Sensitive Polymorphic Effects on an algebraic characterization of sequential effect systems has been accepted to ECOOP 2017!
  • I'm on the Academic Panel for the ECOOP 2017 Doctoral Symposium. If you're a doctoral student in PL looking for feedback on your work, please consider submitting!
  • I will present Verifying Invariants of Lock-Free Data Structures Using Rely-Guarantee References at the TOPLAS session at PLDI 2017!
• 2/17: I'm on the IWACO 2017 Program Committee. Please consider submitting!
• 1/17: My paper on verifying invariants of lock-free data structures using rely-guarantee references, with colleagues from University of Washington and Microsoft Research, was accepted to ACM TOPLAS!
• 1/17: I'm teaching CS451: Software Engineering this term.
• 9/16: I'm teaching two sections of SE320: Software Verification and Validation this term.
• 8/16: My paper on type inference for static compilation of JavaScript with colleagues from Samsung Research was accepted to OOPSLA 2016!
• 5/16: I'm on the ECOOP 2017 Program Committee. You should submit!
• 3/16: My paper on trace typing with colleagues from Aarhus, Samsung Research, and UC Berkeley was accepted to ECOOP 2016!
• 2/16: I'm on the IWACO 2016 Program Committee. Please consider submitting!
• 1/16: I'm teaching a grad seminar CS T680 on program verification: type theory, model checking, symbolic execution, Hoare logic and proof assistants.
• 10/15: I'm on the ASE 2016 Tool Demo Track Program Committee. Please consider submitting!
• 10/15: I'm on the PLDI 2016 External Review Committee. Please consider submitting!
• 8/15: I'm on the ECOOP 2016 External Review Committee. Please consider submitting!

Brief Bio

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 and the Solaris kernel group at Sun Microsystems, and have been both a full-time employee (before grad school) and intern (during grad school) with the Midori operating system incubation group at Microsoft. Prior to joining Drexel I was a researcher (Senior Research Engineer) at Samsung Research America in the Advanced Programming Tools group.