Lee Pike

Site Links

• Bio
  
• Experience
• Education
• Service
• Interns and Students
• Research
• Publications
• Talks
  
• Press
  
• Misc.
  

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

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

• Project: ``Vision Control for a UAV'', 2013
• Project: ``Why do airplanes crash?'', 2012
• Project: ``Building an open-source UAV '', 2011

Research Projects

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

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

• 2018
• • D. Cofer, A. Gacek, J. Backes, M. W. Whalen, L. Pike, A. Foltzer, M. Podhradsky, G. Klein, I. Kuz, J. Andronick, G. Heiser, D. Stuart}. A Formal Approach to Constructing Secure Air Vehicle Software. IEEE Computer, issue 11, vol. 51, 2018.
  • Benjamin F. Jones, Lee Pike, Srivatsan Varadarajan, and Brendan Hall. Language for Unified Verification and Implementation for Distributed Avionics. Journal of Aerospace Information Systems, 2018.
  • Mark Tullsen, Lee Pike, Nathan Collins, Aaron Tomb. Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System. Computer-Aided Verification (CAV), 2018.

• 2017
• • Georges-Axel Jaloyan and Lee Pike. Lock Optimization for Hoare Monitors in Real-Time Systems. The 17th International Conference on Application of Concurrency to System Design (ACSD), 2017.
  • Benjamin F. Jones and Lee Pike. Modular model-checking of a Byzantine fault-tolerant protocol. Accepted at the NASA Formal Methods Symposium (NFM), 2017. Nominated for extended version to submitted to the Journal of Automated Reasoning (declined).
  • Lee Pike, Jamey Sharp, Mark Tullsen, Patrick C. Hickey, and James Bielman. Securing the automobile: the next steps. Accepted at IEEE Software special issue on automotive software, 2017.

• 2016
• • Lee Pike. Hints for High-Assurance Cyber-Physical System Design. IEEE Cybersecurity Development (SecDev), 2016.
  • Lee Pike, Pat Hickey, Trevor Elliott, Eric Mertens, and Aaron Tomb. TrackOS: a Security-Aware Real-Time Operating System. 16th Intl. Conference on Runtime Verification, 2016.

• 2015
• • Lee Pike, Jamey Sharp, Mark Tullsen, Patrick C. Hickey, and James Bielman. Securing the automobile: a comprehensive approach. Galois Technical Report, 2015.
  • Jonathan Laurent, Alwyn Goodloe and Lee Pike. Assuring the guardians. Runtime Verification, 2015.
  • Trevor Elliott, Lee Pike, Simon Winwood, Pat Hickey, James Bielman, Jamey Sharp, Eric Seidel, John Launchbury. Guilt-free Ivory. Haskell Symposium, 2015.
  • Perry Alexander, Lee Pike, George Coker, Peter Loscocco. Model checking distributed mandatory access control policies. ACM Transactions on Information and System Security, 2015.

• 2014
• • Lee Pike. SmartCheck: automatic and efficient counterexample reduction and generalization. Haskell Symposium, 2014.
  • Patrick C. Hickey, Lee Pike, Trevor Elliott, James Bielman, John Launchbury. Building embedded systems with embedded DSLs (experience report). Intl. Conference on Functional Programming, 2014.
  • Lee Pike, Patrick C. Hickey, James Bielman, Trevor Elliott, Thomas DuBuisson, John Launchbury. Programming languages for high-assurance autonomous vehicles (extended abstract). Programming Languages meets Programming Verification (PLPV), Jan. 2014. Invited paper.

• 2013
• • Matthew Clark, Xenofon Koutsoukos, Ratnesh Kumar, Insup Lee, George Pappas, Lee Pike, Joseph Porter, Oleg Sokolsky. A Study on Run Time Assurance for Complex Cyber Physical Systems. AFRL technical report ADA585474, 2013.
  • Lee Pike, Nis Wegmann, Sebastian Niller, Alwyn Goodloe. Copilot: monitoring embedded systems. Innovations in Systems and Software Engineering, Special Issue on Software Health Management, 2013.

• 2012
• • Lee Pike, Nis Wegmann, Sebastian Niller, Alwyn Goodloe. Experience report: a do-it-yourself high-assurance compiler. International Conference on Functional Programming (ICFP), Sept. 2012. SIGPLAN Comm. of the ACM "Research Highlights" nominated paper.
  • Lee Pike, Nis Wegmann, Sebastian Niller, Alwyn Goodloe. Copilot: Monitoring Embedded Systems. NASA Contractor Report NASA/CR-2012-217329, January 2012.

• 2011
• • Darren Abramson and Lee Pike. When formal systems kill: computer ethics and formal methods. APA Newsletter on Philosophy and Computers, Fall 2011.
  • Lee Pike, Sebastian Niller, and Nis Wegmann. Runtime Verification for Ultra-Critical Systems. 2nd Intl. Conference on Runtime Verification, 2011.
  • Lee Pike. Pervasive formal verification in control system design (panel discussion). Formal Methods in Computer Aided Design (FMCAD'11), 2011.
  • Iavor Diatchki and Lee Pike and Levent Erkök. Practical considerations in control-flow integrity monitoring. 2nd Intl. Workshop on Security Testing (SECTEST), 2011.
  • Geoffrey M. Brown and Lee Pike. Automated verification and refinement for physical-layer protocols. Formal Aspects of Computing, 2011.

• 2010
• • Lee Pike, Alwyn Goodloe, Robin Morisset, and Sebastian Niller. Copilot: A Hard Real-Time Runtime Monitor. 1st Intl. Conference on Runtime Verification (RV'2010), 2010. Springer.
  • Lee Pike. Schrödinger's CRCs (Fast Abstract). 40th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2010), 2010.
  • Alwyn Goodloe and Lee Pike. Monitoring distributed real-time systems: a survey and future directions. NASA Contractor Report NASA/CR-2010-216724, 2010.

• 2009
• • Lee Pike, Geoffrey M. Brown, and Alwyn Goodloe. Roll your own test bed for embedded real-time protocols: a Haskell experience. Haskell Symposium, 2009.
  • Lee Pike. Post-hoc separation policy analysis with graph algorithms. Workshop on Foundations of Computer Security (FCS'09), 2009.
  • Alwyn Goodloe and Lee Pike. Toward monitoring fault-tolerant embedded systems (extended abstract). International Workshop on Software Health Management (SHM'09), 2009.

• 2007
• • Lee Pike. Model checking for the practical verificationist: a user's perspective on SAL. Automated Formal Methods (AFM07), 2007.
  • [Best paper award] Lee Pike. Modeling time-triggered protocols and verifying their real-time schedules. 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. 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. Disproving '06 (Participants' proceedings), 2006.
  • Lee Pike. A note on inconsistent axioms in Rushby's "Systematic formal verification for fault-tolerant time-triggered algorithms". 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. 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. Designing Correct Circuits (DCC'06) (Participants' Proceedings), 2006.
  • Geoffrey Brown and Lee Pike. Easy parameterized verification of biphase and 8N1 protocols. 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. 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. 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. 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. Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems (FORMATS-FTRTFT), volume 3253 of LNCS, pages 167--182, 2004. Springer.

• Miscellaneous:
• • Lee Pike. Towards automotive software health management (position paper). Workshop on Developing Dependable and Secure Automotive Cyber-Physical Systems from Components, 2011.
  • Lee Pike. Rethinking Formal Methods. Letter to the Editor, IEEE Computer, pp. 6-9, vol. 43, 2010.
  • Lee Pike, Don Stewart, and John Van Enk. Unmanned autonomous verification and validation (position paper). Mixed Criticality Workshop of the RTAS Symposium, 2009.
  • 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.
  • 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!
  
• • Lee Pike. Architecture Needs Behavior. (Draft paper).
  • Lee Pike. A Protocol for Anonymous and Private Federated Search. (Draft paper).
  • Lee Pike. Decomposing Correctness Proofs of Fault-Tolerant Algorithms. (Draft paper).
  • Lee Pike. How to pretty-print a long formula. In progress (draft paper and the pretty-printer are available).

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.

• 2013
• • Keynote: Building a High-Assurance Unpiloted Air Vehicle. Intl. Conference on Formal Methods and Models for Codesign (MEMOCODE'13). Portland, Oregeon, 2013.
  • TrackOS: A Security-Aware RTOS High Confidence Software and Systems Conference. May 2013.

• 2012
• • A Do-It-Yourself High-Assurance Compiler.
    • Kestrel Seminar, Nov. 2012
    • Keynote: Systems Software Verification Conference. Sydney, Australia, Nov. 2012.
    • Keynote: Midwest Verification Day. Lawrence, Kansas, Sept. 2012.
  • Experience Report: a Do-It-Yourself High-Assurance Compiler. Intl. Conference on Functional Programming (ICFP). Copenhagen, Denmark, 2012.
  • TrackOS: a Security-Aware RTOS. Safe and Secure Systems and Software Symposium (S5), June 2012.

• 2011
• • Runtime monitoring: real-time constraints. University of Pennsylvania, Dec. 2011.
  • Panel discussion: pervasive formal verification in control system design. FMCAD panel, Nov 2011.
  • High-level views on low-level software verification. Mini-worshop on formal methods and control systems. Georgia Institute of Technology, Oct. 2011.
  • Runtime Verification for Ultra-Critical Systems. 2nd Intl. Conference on Runtime Verification, 2011.
  • >11+ years of formal methods at Galois, Inc.
    • SRI, International, Sept. 2011.
    • NASA Ames, Sept. 2011.
  • Real-time runtime monitoring (slides)
    • High-Confidence Software and Systems, May 2011.
    • NASA Aviation Safety Annual Technical Meeting, May 2011.

• 2010
• • Copilot: A Hard Real-Time Runtime Monitor
    • Galois Technical Seminar, November 2010.
    • Conference on Runtime Verification, November, 2010.
  • Analyzing a cross-domain component: lessons learned. Software Certification Consortium, August 2010.
  • Cryptol, the language of cryptography.
  • • Saarland Univerity. July, 2010.
    • National Institute of Aerospace. June, 2010.
  • Temporal refinement using SMT and model checking with an application to physical-layer protocols. Dagstuhl Seminar 10271: Verification over discrete-continuous boundaries. July, 2010. (Proceedings here.)
  • Schrödinger's CRCs (Fast Abstract). 40th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2010), 2010.
  • An Introduction to Formal Methods and their Application. Portland State UniversityAssociation for Computing Machinery Seminar. May, 2010

• 2009
• • Roll your own test bed for embedded real-time protocols: a Haskell experience. Haskell Symposium 2009.
  • Post-hoc separation policy analysis with graph algorithms. Workshop on Foundations of Computer Security (FCS'09), 2009.
  • An introduction to Cryptol. 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, 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.
    • 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.

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

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