Lee Pike

Site Links

• Bio
  
• Experience
• Education
• Service
• Research
• Publications
• Talks
  
• Misc.
  
• 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

• 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'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

• 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' AAMP7^TM 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.

• 2009
• Alwyn Goodloe and Lee Pike. Monitoring distributed real-time systems: a survey and future directions. To be published as a NASA Contractor Report.
• Geoffrey M. Brown and Lee Pike. Automated verification and refinement for physical-layer protocols. Accepted at Formal Aspects of Computing (Springer).
• Lee Pike, Geoffrey M. Brown, and Alwyn Goodloe. Roll your own test bed for embedded real-time protocols: a Haskell experience. In Haskell Symposium, 2009.
• Lee Pike. Post-hoc separation policy analysis with graph algorithms. In Workshop on Foundations of Computer Security (FCS'09), 2009.
• Alwyn Goodloe and Lee Pike. Toward monitoring fault-tolerant embedded systems (extended abstract). In International Workshop on Software Health Management (SHM'09), 2009.
• Lee Pike, Don Stewart, and John Van Enk. Unmanned autonomous verification and validation (position paper). In Mixed Criticality Workshop of the RTAS Symposium, 2009.
• Lee Pike. How to pretty-print a long formula. In progress (draft paper and the pretty-printer are available).
• Darren Abramson and Lee Pike. When formal systems kill: computer ethics and formal methods. In progress (draft paper available).

• 2008
• Lee Pike. High-Confidence Bus Architectures: The Backbone of Automotive Cyber-Physical Systems (position paper). National Workshop on High-Confidence Automotive Cyber-Physical Systems, 2008.

• 2007
• Lee Pike. Model checking for the practical verificationist: a user's perspective on SAL. In Automated Formal Methods (AFM07), 2007.
• [Best paper award] Lee Pike. Modeling time-triggered protocols and verifying their real-time schedules. In Formal Methods in Computer Aided Design (FMCAD 2007), 2007.
• Geoffrey Brown and Lee Pike. Temporal refinement using SMT and model checking with an application to physical-layer protocols. In Fifth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'2007), 2007.

• 2006
• Lee Pike, Paul Miner, and Wilfredo Torres-Pomales. Diagnosing a failed proof in fault-tolerance: a disproving challenge problem. In Disproving '06 (Participants' proceedings), 2006.
• Lee Pike. A note on inconsistent axioms in Rushby's "Systematic formal verification for fault-tolerant time-triggered algorithms". In IEEE Transactions on Software Engineering, 32(5): 347-348, 2006.
• Lee Pike, Mark Shields, and John Matthews. A verifying core for a cryptographic language compiler. In Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006.
• Geoffrey Brown and Lee Pike. "Easy" parameterized verification of cross clock domain protocols. In Designing Correct Circuits (DCC'06) (Participants' Proceedings), 2006.
• Geoffrey Brown and Lee Pike. Easy parameterized verification of biphase and 8N1 protocols. In 12th International Conference on Tools and Algorithms for the Construction and Analysis of Algorithms (TACAS'06), volume 3920 of LNCS, pages 58--72, 2006. Springer.
• Lee Pike. Formal Verification of Time-Triggered Systems. Ph.D dissertation. Indiana University, 2006.

• 2005
• Lee Pike and Steven D. Johnson. The formal verification of a reintegration protocol. In EMSOFT '05: Proceedings of the 5th ACM international conference on Embedded software, pages 286--289, 2005. ACM Press.
• Lee Pike. Real-time system verification by k-induction. NASA Technical Memorandum TM-2005-213751, 2005.

• 2004
• Lee Pike, Paul Miner, and Wilfredo Torres-Pomales. Model checking failed conjectures in theorem proving: a case study. NASA Technical Memorandum TM-2004-213278, 2004.
• Lee Pike, Jeffrey Maddalon, Paul Miner, and Alfons Geser. Abstractions for fault-tolerant distributed system verification. In Theorem Proving in Higher Order Logics (TPHOLs), volume 3223 of LNCS, pages 257--270. 2004. Springer.
• Gerard Allwein, Hilmi Demir, and Lee Pike. Logics for classes of boolean monoids. In Journal of Logic, Language and Information, 13(3): 241--266, 2004.
• Paul Miner, Alfons Geser, Lee Pike, and Jeffery Maddalon. A unified fault-tolerance protocol. In Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems (FORMATS-FTRTFT), volume 3253 of LNCS, pages 167--182, 2004. Springer.

• Miscellaneous:
  
• 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). In Essays in Philosophy, A Biannual Journal, 2(2), 2001.

Talks

• 2009
• Roll your own test bed for embedded real-time protocols: a Haskell experience. At the Haskell Symposium 2009.
• Post-hoc separation policy analysis with graph algorithms. At the Workshop on Foundations of Computer Security (FCS'09), 2009.
• An introduction to Cryptol. At The Aerospace Corporation, 2009.
• Building consensus: foundations of monitoring ultra-reliable systems. IVHM Software Health Management Technical Interchange Meeting, 2009.
• Unmanned autonomous verification and validation. Mixed Criticality Workshop of the RTAS Symposium, 2009.

• 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.
  • Automated Formal Methods (AFM'07). Atlanta, Georgia, USA. November, 2007.
  • Galois Technical Seminar. Beaverton, Oregon. November, 2007.
• 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:
• Propositional proving in PVS.
• Predicate proving in PVS.
• SRI's Symbolic Analysis Laboratory (SAL).
• 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.

• Older talks:
  
• Begging the question, objections, and evidence. Inland Northwest Philosophy Conference (INPC), Moscow, Idaho. 2000.
  
• The duck-rabbit, Duchamp's fountain, and the death penalty.  Building Bridges: Aesthetics and Ethics Conference, Carbondale, Illinois. 2000.

Misc.

• Coauthors:
  • Darren Abramson, Dalhousie University, Halifax, Canada.
  • Gerard Allwein, Naval Research Laboratory (NRL), Washington D.C.
  • Geoffrey Brown, Indiana University
  • Hilmi Demir, Bilkent University, Ankara, Turkey
  • Alfons Geser, Institut für Prozessinformatic und Leittechnik
  • Alwyn Goodloe, National Institute of Aerospace
  • Steve Johnson, Indiana University
  • Jeffrey Maddalon, NASA Langley Research Center
  • John Matthews, Galois, Inc.
  • Paul Miner, NASA Langley Research Center
  • Mark Shields, Microsoft
  • Wilfredo Torres-Pomales, NASA Langley Research Center
  
  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).

• Formal methods:
  • Coinduction: Here's a simple tutorial on coinductive definitions and coinductive reasoning in PVS 3.2: coinduction.dmp. For a more complete tutorial, I enjoyed Bart Jacob and Jan Rutten's A tutorial on (co)algebras and (co)induction.
  • SAL scripts: I've posted some simple SAL (SRI's model-checker) bash scripts to automate its usage.