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 Dept. of Defense agencies. His
research focuses on applying techniques from functional programming,
run-time verification, and formal verification as applied to 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: 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.
- Here's my LinkedIn
profile; I find this more convenient than business cards.
Experience
- Research & Development, Galois, Inc., August, 2005 -
present.
- Research Scientist, NASA Langley Formal
Methods Group, September, 2003 - August, 2005.
- Visiting Researcher, National Institute of
Aerospace Formal Methods Group, May - August, 2003.
- Associate Instructor, Indiana
University, Bloomington, August, 2000 - May, 2003.
Education
- Ph.D, Computer Science,
Indiana University, Bloomington, May, 2006.
- Ph.D Program, Philosophy, Indiana University,
Bloomington, August 2000 - May, 2003 (unfinished -- all double
Ph.D coursework completed).
- M.S. Computer Science,
Indiana University, Bloomington, May, 2003.
- B.A. Philosophy,
University of Idaho, May, 2000.
Service
- ASWEC'13 (24th
Australian Software Engineering Conference), Program
Committee.
- ITP'13 (4th
International Conference 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), 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; 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; Software, Testing, Verfication, and
Reliability; and Formal Methods in System Design.
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. 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.
- Miscellaneous:
-
- Lee Pike.
Rethinking Formal Methods. Letter to the Editor, IEEE
Computer, pp. 6-9, vol. 43, 2010.
- Jeffrey R. DiLeo, Green Musselman, and Lee Pike. Introduction to philosophy: a learning
guide. Indiana School of Continuing Studies, 2003.
- Lee Pike. Book review:
Husserl or Frege? meaning, objectivity and mathematics (by
Claire Ortiz Hill and Guillermo E. Rosado Haddock). Essays in
Philosophy, A Biannual Journal, 2(2), 2001.
- Drafts (please let me know of comments or
corrections)
-
Talks
- 2008
-
- Monitor synthesis for software
health managementfor software health management. Invited panel
presentation at NASA
Aviation Safety Technical Conference, Denver, Colorado.
October, 2008.
- Pretty-printing a
really long formula (or, wat a mathematician could learn from
Haskell).
Galois Technical Seminar, Portland, Oregon. September,
2008.
- Cryptol: specification, implementation, and verification of
high-grade cryptographic applications. Invited talk at Computer Aided Cryptography
Engineering (CACE) Meeting, Porto, Portugal. July, 2008.
(Disclaimer: the talk overviewed very few of my own contributions
and very many of my colleagues'
contributions.)
- When formal systems kill:
computer ethics and formal methods. Galois Technical
Seminar, Beaverton, Oregon. June, 2008.
- Model checking for the practical
verificationist: a user's perspective on SAL. The Sixth NASA
Langley Formal Methods Workshop (LFM 2008). Newport News,
Virginia. April, 2008.
- 2007
-
- [Best paper award] Modeling time-triggered protocols and
verifying their real-time schedules.
- Formal Methods in Computer-Aided Design (FMCAD'07).
Austin, Texas, USA. November, 2007.
- Galois Technical Seminar. Beaverton, Oregon. November,
2007.
- Model checking for the practical
verificationist: a user's perspective on SAL.
- When formal systems kill:
computer ethics and formal methods. North American Computers and
Philosophy Conference (NA-CAP). Chicago, Illinois. July,
2007. (My coauthor, Darren Abramson, also presented this paper at
the European Computing
and Philosophy Conference (ECAP), Enschede, The
Netherlands, June, 2007).
- Temporal refinement using
SMT and model checking with an application to physical-layer
protocols.
- ACM-IEEE International Conference on Formal Methods and
Models for Codesign (MEMOCODE'2007). Nice, France. May,
2007.
- University of Kansas, Lambda Group.
Lawrence, Kansas. April, 2007.
- Galois Technical Seminar. Beaverton, Oregon. March,
2007.
- 2006
-
- Temporal refinement using
SMT and model checking with an application to physical-layer
protocols. National
Institute of Aerospace. Hampton, Virgina. November,
2006.
- Easy parameterized verification
of Biphase Mark and 8N1 protocols. Pragmatics of Decision
Procedures in Automated Reasoning (PDPAR '06), Seattle.
August, 2006.
- Diagnosing a failed proof
in fault-tolerance: a disproving challenge problem.
Disproving Workshop'06, Seattle (a FLoC event). August,
2006.
- A verifying core for a
cryptographic language compiler.
- Sixth International Workshop on the ACL2 Theorem Prover and
its Applications, Seattle (a FLoC event). August, 2006.
-
Automated Reasoning Group, University of Cambridge.
November, 2006.
- Easy parameterized verification of
Biphase Mark and 8N1 protocols. 12 International Conference
on Tools and Algorithms for the Construction and Analysis of
Algorithms (TACAS'06), Vienna. March, 2006.
- 2005
-
- A framework for the formal verification of
time-triggered systems. Dissertation Defense Public
Presentation, Indiana University. December, 2005.
- Lectures I gave at the 2005 NASA
Langley/NIA PVS Course:
-
- The formal verification of a
reintegration protocol.
- Strategic CAD Labs, Intel, Hillsboro, OR. June,
2005.
- Advanced Technology Center, Rockwell Collins, Cedar
Rapids, Iowa. May, 2005.
- Center for High Assurance
Computer Systems, Naval Resarch Laboratory, Washington, D.C.
April, 2005.
- SPIDER: a fault-tolerant bus
architecture. Microprocessor Technology Laboratory,
Intel, Santa Clara, California. May, 2005.
- How
not! to axiomatize time-triggered systems.
NASA Langley/NIA Formal Methods
Coffee Series Colloquium, NASA Langley Research Center.
April, 2005.
- Verifying real-time systems by
k-induction. Reliable Digital
Avionics Branch Talk, NASA Langley Research Center.
February, 2005.
- 2004
-
- The philosophy of formal
methods. Philosophy
Colloquium, California State University, Fresno. September,
2004.
- Formal methods in the SPIDER
project. Software Engineering
Seminar, California State University, Fresno. September,
2004.
- Abstractions for
fault-tolerant distributed system verification. Theorem Proving in Higher-Order Logics
(TPHOLs), Park City, Utah. September, 2004.
- Abstractions for
fault-tolerant distributed system verification (in higher-order
logic). Logic Group Colloquium, Indiana
University, Bloomington. April, 2004.
- Open problems in the formal
verification of SPIDER. Oral
Examination Presentation, Indiana University,
Bloomington. April, 2004.
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).
|
