Lee Pike

Site Links

• Bio
  
• Experience
• Education
• Service
• Research
• Publications
• Talks
  
• Misc.
  
• Links

Short Bio

I work 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, at Galois 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 also check out the Galois Galois Blog, which particularly highlights our seminar series.

Here's my LinkedIn profile; I find this more convenient than business cards.

Experience

• R&D Engineer, 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'09 (20th Australian Software Engineering Conference), Program Committee.
• FMCAD'08 (Formal Methods in Computer-Aided Design), Program Committee and Publicity Chair. FMCAD will be located downtown Portland, Oregon November 17-20, 2008.
• AFM'08 (Automated Formal Methods), Program Committee.
• AFM'07 (Automated Formal Methods), Program Committee.
• I've also been an "external reviewer" for CAV, TPHOLs, CHARME, EMSOFT, ICCD, and PADL in the past.

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. The research team includes myself as the Principal Investigator, Cesar Munoz as the Co-PI (NIA), and Alwyn Goodloe as a Research Scientist (NIA). 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

• 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.
• Darren Abramson and Lee Pike. When formal systems kill: computer ethics and formal methods. Submitted (journal article). Comments solicited!
• Geoffrey M. Brown and Lee Pike. Automated verification and refinement for physical-layer protocols. Submitted (journal article), 2007. Comments solicited!

• 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

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