My Picture

Lee Pike

Web page http://www.cs.indiana.edu/~lepike/ Phone +1 503.808.7185
Email

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.

Experience

Education

Service

  • 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.
  • 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.

Publications

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).

Talks

  • 2014
    • Keynote: Programming Languages for High-Assurance Autonomous Vehicles. Programming Languages Meets Program Verification (PLPV'14). San Diego, California, 2014.

Press

Misc.

  • 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.