My Picture

Lee Pike

Web page https://leepike.github.io
Email

Public Key GnuPG

Site Links








Short Bio

Lee Pike is currently a Principal Applied Scientist at Amazon Web Services. He previously led the compiler team at Groq, Inc. Before that, he directed the Cyber-Physical Systems program at Galois, Inc. He has been the PI on externally-funded research contracts funded by NASA, DARPA, AFRL, DOT, and other agencies and Fortune 100 companies. 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.
  • Some of my personal software projects are on GitHub.
  • Here's my LinkedIn profile; I find this more convenient than business cards.

Experience

  • Principal Applied Scientist, Amazon Web Services, February 2019 - present.
  • 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

Service

  • 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 are a few 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).
  • 2019
    • Trevor Elliott, Mohammed Alshiekh, Laura Humphrey, Lee Pike, and Ufuk Topcu. Salty–A Domain Specific Language for GR(1) Specifications and Designs. Accepted at IEEE Intl. Conf. of Robotics and Automation, 2019.

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.

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.