Site Links
|
|
Short
Bio
I work in Research & Development at
Galois, Inc., specializing
in software-intensive critical systems. My work is focused on applying techniques from functional programming,
run-time verification, and formal methods to raise the
level of abstraction in embedded systems, including
operating systems, compilers, cryptography, avionics, and
control systems. Previously, I was a research scientist
in 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
- 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
- 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.
- 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,
and Annals of Mathematics and Artificial Intelligence,
the Haskell Symposium, NA-CAP (the North American
Conference on Computing and Philosophy), and
Innovations in Systems and Software Engineering
(journal).
Research
Projects
The following are a few of the public
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.
- 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).
|
