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

I have worked in Research & Development at Galois, Inc. since 2005. My area of research is dependable systems, including both safety-critical and security-critical systems. I focused on formal (i.e., mathematical) analysis techniques for dependable systems, including the use of model-checking, mechanical theorem-proving, and decision procedures, but I have also worked in protocol design. My work also touches on the areas of programming languages, virtualization, online monitors, and realtime systems. In addition, I've managed research business-development and hiring in Engineering. Previously, I was a research scientist with the NASA Langley Formal Methods Group. I have 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've also started a blog mainly focusing on open questions in my area of research.
  • You can also check out the Galois blog, which highlights the technical going-ons at the company.
  • Here's my LinkedIn profile; I find this more convenient than business cards.

Experience

Education

Service

  • ASWEC'10 (21st Australian Software Engineering Conference), Program Committee.
  • ITP'10 (Interactive Theorem Proving), Programm Committee. (ITP merges TPHOLs and the ACL2 Workshop.)
  • 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, Journal of Software and Systems Modeling, and Annals of Mathematics and Artificial Intelligence, the Haskell Symposium, and NA-CAP (the North American Conference on Computing and Philosophy).

Research Projects

The following are some (but not all) of the research projects to which I am currently contributing to or 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. If you're interested in finding out more about the research or are interested in collaborating, don't hesitate to drop me an email.
  • 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.

Talks

Misc.

  • Coauthors:
    Incidentally, 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.