My Picture

Lee Pike

Web page Phone +1 503.808.7185

Fax +1 503.350.0833
Public Key GnuPG NEW!!
Mailing Address
Galois, Inc.
421 SW 6th Ave.
Suite 300
Portland, OR 97204, USA

Site Links

Short Bio

Lee Pike manages the Cyber-Physical Systems program at Galois, Inc., a company specializing in software-intensive critical systems. He has been the PI on approximately $10 million of R&D projects funded by NASA, DARPA, and other federal agencies. His research focuses on applying techniques from functional programming, run-time verification, and formal verification to the areas of operating systems, compilers, cryptographic systems, avionics, and control systems. Previously, he was a research scientist in the NASA Langley Formal Methods Group and has a Ph.D in Computer Science from Indiana University.

  • You can check out my papers, talks, and projects below. You can subscribe to an RSS feed of my publications.
  • I have a blog. You can also check out the Galois blog, which highlights the technical going-ons at the company.
  • Some of my personal software projects are on GitHub. Galois' open-source projects are also on Galois' GitHub page.
  • Here's my LinkedIn profile; I find this more convenient than business cards.




  • RV'16 (Intl. Conference on Runtime Verification), Program Committee
  • EMBEDDED'16 (The International Symposium on Advances in Embedded Systems and Applications), Program Committee
  • NFM'16 (NASA Formal Methods Symposium), Program Committee
  • Denmark Innovation Fund, Expert Reviewer, 2015
  • IEEE Communications Magazine, special issue on wireless communications, networking, and positioning with unmanned aerial vehicles, Guest Editor, 2015
  • ICESS'15 (12TH IEEE International Conference on Embedded Software and Systems), Program Committee
  • NSF Panelist, 2015
  • FMCAD'15 (Formal Methods in Computer-Aided Design), Program Committee
  • ICCPS'15 (International Conference on Cyber-Physical Systems), Program Committee
  • RTSS'14 (IEEE Real-Time Systems Symposium), Program Committee
  • NSF Panelist, 2014
  • FMCAD'14 (Formal Methods in Computer-Aided Design), Program Committee
  • Haskell Symposium 2014, Program Committee
  • NFM'14 (NASA Formal Methods Symposium), Program Committee
  • ITP'14 (Intl. Conf. on Interactive Theorem Proving), Program Committee
  • RV'14 (Intl. Conf. on Runtime Verification), Program Committee
  • ACL2'14, Program Committee
  • Workshop on Theorem Proving in Certification, Co-organizer, 2013
  • NSF Panelist, 2013
  • FMCAD'13 Formal Methods in Computer-Aided Design), Program Committee
  • ASWEC'13 (24th Australian Software Engineering Conference), Program Committee
  • ITP'13 (4th Intl. Conf. on Interactive Theorem Proving), Program Committee
  • FMCAD'12 (Formal Methods in Computer-Aided Design), Program Committee
  • Workshop on Theorem Proving in Certification, Co-organizer, 2011.
  • FMCAD'11 (Formal Methods in Computer-Aided Design), Program Committee
  • ITP'11 (2nd International Conference on Interactive Theorem Proving), Program Committee
  • Workshop on Theorem Proving in Certification, Co-organizer, 2010
  • FMCAD'10 (Formal Methods in Computer-Aided Design), Program Committee
  • ASWEC'10 (21st Australian Software Engineering Conference), Program Committee
  • ITP'10 (Interactive Theorem Proving), Program Committee
  • AFM'09 (Automated Formal Methods), Program Committee
  • FMCAD'09 (Formal Methods in Computer Design), Program Committee
  • ASWEC'09 (20th Australian Software Engineering Conference), Program Committee
  • FMCAD'08 (Formal Methods in Computer-Aided Design), Program Committee and Publicity Chair.
  • AFM'08 (Automated Formal Methods), Program Committee
  • AFM'07 (Automated Formal Methods), Program Committee
  • I've also reviewed for CAV, TPHOLs, CHARME, EMSOFT, ICCD, PADL, ICFP, Journal of Software and Systems Modeling, Annals of Mathematics and Artificial Intelligence, the Haskell Symposium, NA-CAP (the North American Conference on Computing and Philosophy), Innovations in Systems and Software Engineering, Formal Methods in System Design, and Software, Testing, Verfication, and Reliability.

Research Projects

The following are a few of the research projects to which I have contributed.
  • Correct-by-construction planning synthesis. I am the PI on a joint project with Ufuk Topcu at the University of Texas funded by AFRL. We are addressing the problem of creating plans involving multiple coordinating robotic vehicles. An emphasis on our work is how create plans that are correct, scalable, and easy to specify. As well, our focus is planning in the context of real-world constraints, including faults and real-time deadlines. Our approach is a correct-by-construction approach, synthesizing plans from high-level DSLs.

  • Architectural Framework for Integrated Refinement Modeling (AFFIRM). Funded by NASA, and a partnership between Honeywell and Galois, Inc. I am the PI. We are investigating refinement strategies for modeling and synthesizing fault-tolerant distributed systems.

  • High-Assurance Cyber Military Vehicles (HACMS). I am the PI for Galois on a team led by Rockwell Collins. Check out the SMACCMPilot webpage, an open-source autopilot we are building using Haskell embedded DSLs, model-checking, and other formal approaches.

  • Autonomous Systems Hardening (ASH). The problem this project addresses is how to perform control-flow integrity in the context of hard real-time systems. Our approach was to build TrackOS, a control-flow monitoring real-time operating system.

  • Runtime Verification study. As a subject matter expert for the Air Force Research Lab, I participated in a study on the use of runtime verification for cyber-physical systems. Our final report is here.

  • Monitor Synthesis for Software Health Management. NASA has awarded Galois, Inc. together with the National Institute of Aerospace (NIA), a research contract to investigate monitor synthesis for software health management (here's the press release from Reuters). The research team includes myself as the Principal Investigator and Alwyn Goodloe at the NIA as the Co-PI. The award runs through the end of 2011, and we are investigating the formal synthesis of online monitors from requirements specifications. The research will focus on safety properties and real-time properties of distributed systems. We built the Copilot language in this project; see it's GitHub page for more information.

  • SHADE (Secure, High-Assurance Development Environment). I helped build some of the verifying infrastructure for a high-assurance compiler from a domain-specific cryptographic language (μCryptol) to Rockwell Collins' AAMP7TM microprocessor. The compiler was designed to issue both machine code and a machine-checked proof that the machine code program implements its high-level specification. A paper on the verifier is available. Mark Shields, the designer of the language and the implementor of its compiler, has a technical report describing both.

  • SPIDER (Scalable Processor-Independent Design for Enhanced Reliability). As a member of the SPIDER Team, I was formally verifying an ultra-reliable embedded control system.  The centerpiece of the SPIDER project is the ROBUS (Reliable Optical BUS), an ultra-reliable time-division, multi-access communications bus for long-term and safety-critical missions. The formal methods employed include theorem proving, model checking, cooperating decision-procedures, and interactive synthesis. John Rushby has written a nice report comparing SPIDER with other fault-tolerant busses under development (i.e., Flexray, TTA, and SAFEbus). In fact, many of our verification goals are similar to those discussed in Rushby's report on the formal verification of TTA (a nice summary of the problem domain more generally can be found in Ricky Butler's recent technical report). Additional information and relevant publications can be found at the official SPIDER page and below in the provided publications and talks.


You can subscribe to an RSS feed of my publications.

The links for each title below reveal abstract, bibtex entry, paper, associated slides, and other supporting artifacts (but these days, most public artifacts live on GitHub).
  • 2015
    • Jonathan Laurent, Alwyn Goodloe and Lee Pike. Assuring the Guardians. Runtime Verification, 2015.
    • Trevor Elliott, Lee Pike, Simon Winwood, Pat Hickey, James Bielman, Jamey Sharp, Eric Seidel, John Launchbury. Guilt-free Ivory. Haskell Symposium, 2015.
    • Perry Alexander, Lee Pike, George Coker, Peter Loscocco. Model checking distributed mandatory access control policies. ACM Transactions on Information and System Security, 2015.


  • 2014
    • Programming Languages for High-Assurance Autonomous Vehicles. Safe & Secure Systems and Software Symposium (S5). Dayton, Ohio, 2014.
    • Keynote: Programming Languages for High-Assurance Autonomous Vehicles. Programming Languages Meets Program Verification (PLPV'14). San Diego, California, 2014.



  • I believe my Erdös number is 4: Paul Erdös → Kenneth Kunen → Jon Barwise → Gerard Allwein → Lee Pike.
  • Humor:
    • A colleague once told me that he refused to submit a paper to a conference after once having an earlier outstanding paper of his rejected. Have you ever had your paper rejected from a conference? If so, perhaps you could reject the conference from your paper.
    • Please help support the Free Food Foundation and GNKF (GNFK's Not Kentucky Fried).

The contents herein should not be taken to represent any entity, organization, or person other than Lee Pike.

Notice: due to spamming concerns, the e-mail address on this page has been scripted using Joe Maller's JavaScript.
If you do not see an address opposite the revision date, please either enable
JavaScript in your browser and refresh the page or view the source code for this page.