Research and Engineering
Office: 503.626.6616 x156
Email: atomb (at) galois (dot) com
I have worked in Research and Development at Galois since 2007. My research interests include type systems, programming language semantics, automated program analysis and defect detection. At Galois, I work as both a research engineer and project lead on efforts to develop and apply tools for automated or semi-automated formal verification of software. I also coordinate formal methods research across the company.
I have a B.S., M.S., and Ph.D. in computer science from the University of California, Santa Cruz. My academic work focused on programming language theory, and particularly on the use of advanced programming language technology to improve software reliability. This involves type theory, formal methods, program analysis, and a bit of subjective exploration into what makes languages pleasant to use.
- Detecting Inconsistencies via Universal Reachability Analysis (2012)
- Variably Interprocedural Program Analysis for Runtime Error Detection (2007)
- Space-Efficient Gradual Typing (2007)
- Sage: Hybrid Checking for Flexible Specifications (2006)
- Hybrid Types, Invariants, and Refinements for imperative Objects (2006)
- Automatic Type Inference via Partial Evaluation (2005)