Lee Pike

Site Links

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

Short Bio

I am a R&D Engineer at Galois, Inc. as of August, 2005. Galois is a small company, so there is an opportunity to take on a variety of roles. When I first arrived, I was predominatly a formal methods research engineer. In 2006 and 2007, I was predominatly a project lead for projects investigating security, virtualization, and formal methods. This year, I'm focused on business development in research---please feel free to email me if you have an idea about how you might like to partner with Galois in research. In addition, I have written a few papers in my spare time. Previously, I was a research scientist with the NASA Langley Formal Methods Group, where I was primarily involved in the SPIDER project. I have a Ph.D in Computer Science from Indiana University.

My research interests include all aspects of applying formal methods to safety-critical and security-critical applications. I am particularly interested in applications of infinite-state model-checking, formal methods for evaluation and certification, fault-tolerant and real-time systems, and applied logic.


What are formal methods? In case you are not familiar with formal methods already, here's a short Wikipedia entry, and here's my own three-sentence explanation:

Formal methods are about mathematically proving that computers work correctly. Whereas pure mathematics often involves "deep" proofs, formal methods often involves large and "shallow" proofs. Thus, formal methods research mainly deals with how to model computers mathematically and how to automatically evaluate and generate proofs.

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

• FMCAD'08 (Formal Methods in Computer-Aided Design) PC and Publicity Chair. FMCAD will be located downtown Portland, Oregon November 17-20, 2008. Paper submission deadline: May, 12.
• AFM'08 (Automated Formal Methods) PC. AFM'08 is co-located with CAV in Princeton, New Jersey on July 14. Paper submission deadline: May 25.
• AFM'07 (Automated Formal Methods) PC.

Research Projects

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

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