Site Links
|
|
Short Bio
Lee Pike is currently consulting in automated reasoning, compilers, and neurosymbolic AI as the managing member of
Logothetica LLC. Previously, he has worked in cloud services (at Amazon Web Services), in ML chip design (at Groq, Inc.),
in high-assurance cyber-physical systems research (at Galois, Inc.), and in aerospace formal methods research (at NASA Langley Research Center).
He has over 20 years of experience applying formal methods, programming languages, and software engineering techniques to real-world problems in industry and government,
and has led several teams at this institutions. His Ph.D. is 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.
- Some of my personal software projects are on GitHub.
- Here's my LinkedIn
profile; I find this more convenient than business cards.
Experience
- Founder & Principal Consultant, Logothetica LLC, February 2025 - present
- Principal Applied Scientist, Amazon Web Services, February 2019 - January 2025
- Software Engineer and Compiler Team Lead, Groq, Inc. August, 2017 - December, 2018.
- Prinicipal Investigator, Galois, Inc., August, 2005 -
August, 2017.
- 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
- NFM'25 (NASA Formal Methods Symposium), Program Committee
- HCSS'25 High Confidence Software and Systems Conference, Program Committee
- NFM'24 (NASA Formal Methods Symposium), Program Committee
- HCSS'24 High Confidence Software and Systems Conference, Program Committee
- HCSS'23 High Confidence Software and Systems Conference, Program Committee
- HCSS'22 High Confidence Software and Systems Conference, Program Chair
- HCSS'21 High Confidence Software and Systems Conference, Program Chair
- NFM'18 (NASA Formal Methods Symposium), Program Committee
- DSLDI'17 (Domain-Specific Language Design and Implementation), Program Comittee
- AFM'17 (Automated
Formal Methods), Program Committee
- NFM'17 (NASA Formal Methods Symposium), Program Committee
- FMCAD'17
(Formal Methods in Computer-Aided Design), Program Committee
- Natural Sciences and Engineering Reserach Council of Canada (NSERC) reviewer, 2016
- Air Force Office of Scientific Research, Reviewer, 2016
- NSF Panelist, 2016
- FMCAD'16
(Formal Methods in Computer-Aided Design), Program Committee
- 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,
NA-CAP (the North American Conference on Computing and Philosophy),
Innovations in Systems and Software Engineering, Journal of Formal Methods in
System Design, Journal of Software, Testing, Verfication, and
Reliability, Journal of Automated of Automated Reasoning.
Interns and Students
- Michal Podhradsky (permanently at Galois)
- Georges-Axel Jaloyan (École Normale Supérieure)
- Eric Seidel (Bloomberg)
- Erlend Hamberg (at Soundrop)
- Patrick Hickey (unknown)
- Nis Wegmann (unknown)
- Sebastian Niller (unknown)
- Robin Morisset (École Normale Supérieure Ph.D program)
- Rebekah Leslie (Intel Labs)
I have also mentored the following Portland State undergraduate Capstone projects:
- Project: ``Vision Control for a UAV'', 2013
- Project: ``Why do airplanes crash?'', 2012
- Project: ``Building an open-source UAV '', 2011
Research Projects
The following is an incomplete list of the research projects to which I have
contributed.
- I was PI and wrote an awarded proposal for DARPA Cyber Assured Systems Engineering (CASE). (Declined due to leaving institution.)
-
I am the PI, along with Mark Tullsen, on a project to build verified encoders and decoders for vehicle-to-vehicle specifications.
- 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. 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).
- 2017
-
- Nominated for extended version to submitted to the Journal of Automated Reasoning (declined).
- 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 your thoughts!
-
Talks
- 2017
- Invited presentation: Programming Languages for High-Assurance Vehicles. At the LangSec Workshop.
- 2016
- Invited presentation: Hints for High-Assurance Cyber-Physical System Design. HCCV (Workshop on High-Consequence Control Verification), 2016.
- Keynote: Programming Languages for High-Assurance Vehicles. DARPA Mining and Understanding Software Enclaves (MUSE) PI meeting.
- 2015
-
- Invited panelist: Assurance Tools and Techniques for Trusted Autonomy. At Assurance of Autonomous Systems for Aviation Workshop.
- Invited seminar: Programming Languages for High-Assurance Autonomous Vehicles. Design of Robotics and Embedded systems, Analysis, and Modeling Seminar (DREAMS), UC Berkeley.
- Invited talk: Domain-Specific Languages. Programming Languages Mentoring Workshop (at ICFP).
- Keynote: Programming Languages for High-Assurance Autonomous Vehicles. Conference on Verified Software: Theories, Tools, and Experiments (VSTTE).
- Securing the Automobile: a Comprehensive Approach. Embedded Security in Cars (ESCAR).
- Programming Languages for High-Assurance Autonomous Vehicles.
Sandia National Labs. Livermore, CA.
- 2014
-
- SmartCheck: automatic and efficient counterexample reduction and generalization. Haskell Symposium.
- Programming Languages for High-Assurance Autonomous Vehicles.
Safe & Secure Systems and Software Symposium (S5). Dayton, Ohio.
- Keynote: Programming Languages for High-Assurance
Autonomous Vehicles. Programming Languages Meets Program
Verification (PLPV'14). San
Diego, California, 2014.
- 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, what 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
- Quoted in Can the Federal Government Move to a World Where Software Is Secure by Default?, FedTech Magazine, 2017.
- Quoted in "Unmanned and under attack: Defending UAVs from cyber threats", Jane's International Defence Review, 2017.
- Some of our work on HACMS was featured on 60 Minutes in Feb. 2015.
- I was interviewed on the Security Now podcast, 2015 (skip to around minute 56).
- I've been interviewed by NextGov and GCN about security in embedded systems.
- Our work on HACMS project was featured in the Aerospace America magazine "Year in Review" (December 2014).
- My paper When formal systems
kill: computer ethics and formal methods was featured on the
"front page" of Lambda the Ultimate
Feb., 2012.
- My Copilot
project, sponsored by NASA, was featured in the Aerospace
America magazine "Year in Review" edition (December 2011). Here
is a
link to the page from the magazine mentioning Copilot.
- I was interviewed by Flight
International, in the article, "Control
science tops list of USAF science and technology priorities,"
published May 2010.
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).
|
