NASA Logo, National Aeronautics and Space Administration

Tom Pressburger

Tom Pressburger
Computer Scientist

I work in the Robust Software Engineering Area, headed by Guillaume Brat, which is in the Intelligent Systems Division (Code TI) at NASA Ames.

I worked in the area of software development, analysis and validation tools for the Orion Multi-Purpose Crew Vehicle under Dr. Michael Lowry.

I have worked in the areas of software analysis, software process, software engineering technology infusion, and automated code generation.


Academic Background

My education includes a BS in Mathematics from the California Institute of Technology (Mathematical Logic, Algebra, Theory of Computation, Numerical Analysis), and an MS in Computer Science (AI) from Stanford University. I visited Oxford, Cambridge, and Univ. of Manchester during summers in 1987 and 1989 where I studied formal methods, in particular, Z and VDM, and the algebra of programming.


From 2007 until 2012 I was involved in NASA oversight of the Orion software development tool chain and application of software analysis tools to Orion software. In particular, I analyzed the results of several static analysis tools applied to the flight software for the Pad Abort 1 test flight. I formulated property monitors as hierarchical state machines that implement specification patterns (see "Rapid Property Specification and Checking for Model-Based Formalisms" below). More recently I was involved in applying black-box test case generation and machine learning tools for analyzing the robustness of Guidance, Navigation and Control software for Orion's Exploration Flight Test 1.

I have been the technical representative (COTR) for the contracting officers of several SBIRs related to software tools. I served as COTR for a NASA Research Award about Safety Cases, and as point of contact for a SARP initiative related to Safety Cases; I also reviewed materials that were developed for a tutorial about Assurance Cases.

In 2006, I inherited leading the SARP initiative that produced a practitioner's guidebook to program model checking (see publications, below).

During 2001-2006 I was on the Ames Software Engineering Process Group (EPG) co-representing the Information Sciences directorate. During 2004-2006 I was the alternate representative from Ames to NASA's intercenter Software Working Group; the primary Ames representative was Cyrus Chow. I participated in two class B CMMI appraisals of Ames software projects.

In 2005 I was a member of the Exploration Systems Mission Directorate (ESMD) Computer Software and Automation Integrated Discipline Team (CSA IDT) and, for Constellation, the Software and Avionics Interoperability and Reuse System Integration Group (SAIR SIG). I gathered risks, developed level 2 requirements, and helped write a software reuse study.

I led, with Lawrence Markosian, from 2003 to 2005, the research infusion subgroup of the intercenter Software Working Group. The subgroup's charter was to improve NASA's software engineering practices through research. The subgroup selected mature software engineering research technologies and at the time started over a dozen pilot projects making use of the technologies in NASA software development efforts. The subgroup members at the time were Ben Di Vito (LaRC), Martin Feather (JPL), Michael Hinchey (GSFC), Lawrence Markosian (ARC), Tim Menzies (West Virginia University/IVVF), and Luis Trevino (MSFC), and Wes Deadrick (IVVF) helped out with proposal reviews. The subgroup was awarded "Best New Research" at NASA OSMA SAS'04. See the current research infusion website.

In program synthesis, I have worked on the teams that produced the following systems in the associated domains:

  • Amphion/NAIF: solar system geometry;
  • Amphion/NAV (a precursor to AutoFilter): state estimation using Kalman filters;
  • AutoBayes: statistical analysis;
  • Java PathFinder 1: a Java-to-Promela translator.

Amphion, given a problem specified as a formal, high-level diagram, uses deductive synthesis to generate a program that solves the problem. In that project, I worked on:

  • the logical formalization of the SPICE subroutine library developed by JPL's NAIF group, which is used in planetary exploration;
  • the definition of the abstract graphical specification language;
  • the specification language editor;
  • the tuning of the domain theory so that the deductive engine efficiently processed it (such hand-tuning was to be partially obviated by Meta-Amphion);
  • the transformation into a Fortran program of the result constructed by the deduction engine;
  • the formalization of Amphion's synthesis explanation capability; and
  • the formalization of the decision procedure interface in Meta-Amphion.

Prior to NASA, I worked at the Kestrel Institute where I assisted in the development of several research systems. One such system, called KIDS, devised an algorithm to solve a given problem by applying known algorithmic strategies, e.g. divide-and-conquer. The algorithm could then be optimized by applying program transformations. I worked on the program transformations, the interface architecture, and the language definition. I also worked on the object base and executable specification language used in the software re-engineering platform Software Refinery (TM) provided by Reasoning, Inc. and used it to analyze and transform COBOL programs.

Professional Memberships

  • ACM
  • IEEE Computer Society

Professional Activities

Editorial board, Software: Practice and Experience.

Reviewed papers for these journals: Automated Sofware Engineering, Formal Aspects of Computing, IEEE Transactions on Software Engineering, Journal of Aerospace Information Systems and Software: Practice and Experience.

Industrial Track Program Committee Member, 20th IEEE International Requirements Engineering Conference, Chicago, Illinois, Sep 24-28, 2012.

Program Committee Member, 34th Annual IEEE Software Engineering Workshop, Limerick, Ireland, Jun 20-21, 2011.

Experience Track Committee Member, 28th International Conference on Software Engineering, Shanghai, China, May 20-28, 2006.

Gave presentation on "Verification Technologies" at the NASA Engineering & Safety Center (NESC) Academy course "Software as an Engineering Discipline: Learning from the Past and Looking to the Future with Michael Aguilar and Colleagues", March 15, 2007, online at


"Towards Autonomous Piloting: Communicating with Air Traffic Control", Michael Lowry, Thomas Pressburger, Deborah Dahl, and Michael Dalal. AIAA SciTech Forum, 7-11 January 2019, San Diego, California.

"Design Considerations for a Variable Autonomy Executive for UAS in the NAS", Michael Lowry, Anupa Bajwa, Thomas Pressburger, Adam Sweet, Charles Fry, Michael Dalal, Johann Schumann, Deborah Dahl, Gabor Karsai and Nagabhushan Mahadevan. AIAA SciTech Forum, 2018 AIAA Information Systems-AIAA Infotech@Aerospace, 8-12 January 2018, Kissimmee, Florida, DOI 10.2514/6.2018-1633.

"Simple Sensitivity Analysis for Orion GNC", Tom Pressburger, Brian Hoelscher, Rodney Martin, Kumar Sricharan, AIAA Guidance, Navigation and Control Conference, Boston, MA, Aug 19-22, 2013, paper number AIAA-2013-4954.

"Integrating Statechart Components in Polyglot", Daniel Balasubramanian, Corina S. Pasareanu, Jason Biatek, Thomas Pressburger, Gabor Karsai, Michael Lowry, and Michael W. Whalen, NASA Formal Methods, Lecture Notes in Computer Science volume 7226/2012, p 267-272.

"Rapid Property Specification and Checking for Model-Based Formalisms", Daniel Balasubramanian, Gabor Pap, Harmon Nine, Gabor Karsai, Michael Lowry, Corina Pasareanu and Tom Pressburger, IEEE International Symposium on Rapid System Prototyping (RSP'2011), Karlsruhe, Germany, May 24-27, 2011.

"The Unique Aspects of Simulation Verification and Validation", Danny Thomas, Alexia Joiner, Wei Lin, Michael Lowry, Tom Pressburger, Proc. 2010 IEEE Aerospace Conference, Big Sky, MT, March 6-13, 2010.

AutoBayes Program Synthesis System Users Manual by Johann Schumann, Hamed Jafari, Tom Pressburger, Ewen Denney, Wray Buntine, and Bernd Fischer, NASA/TM—2008–215366, Sep 2008.

Program Model Checking: a Practitioner's Guide by Masoud Mansouri-Samani, Peter Mehlitz, Corina Pasareanu, John Penix, Guillaume Brat, Lawrence Markosian, Owen O'Malley, Thomas Pressburger, and Willem Visser, NASA/TM-2008-214577, January 2008.

"Program Model Checking Using Design-for-Verification: NASA Flight Software Case Study", by L.Z. Markosian, M. Mansouri-Samani, P.C. Mehlitz, and T. Pressburger, Proc. IEEE Aerospace Conference, , Big Sky, MT, March 3-10, 2007.

"Infusing Software Engineering Technology into Practice at NASA", by T. Pressburger, M. Hinchey, M.S. Feather and L. Markosian. Proc. SMC-IT 2006, 2nd IEEE International Conference on Space Mission Challenges for Information Technology, Pasadena, CA, 17-21 July 2006, IEEE Computer Society Press.

"The NASA Software Research Infusion Initiative: Successful Technology Transfer for Software Assurance", by M.G. Hinchey, T. Pressburger, L. Markosian and M.S. Feather. Proc. TT'06, Workshop on Technology Transfer for Software Engineering, International Conference on Software Engineering, Shanghai, China, 20-28 May 2006, ACM Press.

"Infusing Software Assurance Research Techniques into Use", by Thomas Pressburger, Ben Di Vito, Martin Feather, Michael Hinchey, Lawrence Markosian, Luis Trevino, IEEE Aerospace Conference, Big Sky, MT, March 4-11, 2006.

"Amphion/NAV: Deductive Synthesis of State Estimation Software", by Jon Whittle, Jeffrey Van Baalen, Johann Schumann, Peter Robinson, Tom Pressburger, John Penix, Phil Oh, Michael Lowry, Guillaume Brat, Proc. 16th IEEE Conference on Automated Software Engineering, San Diego, California, November 26-29, 2001, pp. 395-399.

"Certifying Domain Specific Policies", by Michael Lowry, Thomas Pressburger, and Grigore Rosu, Proc. 16th IEEE Conference on Robust Software Engineering, San Diego, California, November 26-29, 2001, pp. 81-90.

"The AutoBayes Program Synthesis System - System Description", by Bernd Fischer, Thomas Pressburger, Grigore Rosu, Johann Schumann, Proc. CALCULEMUS 2001: 9th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Siena, Italy, pp. 182-187, June 21-22, 2001.

"Model Checking Java Programs Using Java PathFinder", by K. Havelund and T. Pressburger. International Journal on Software Tools for Technology Transfer (STTT) 2(4):366-381, April 2000.

"Towards Automated Synthesis of Data Mining Programs", by Wray Buntine, Bernd Fischer, Thomas Pressburger, 5th ACM Intl. Conf. on Knowledge Discovery and Data Mining (KDD'99), Aug. 15-18, 1999, San Diego, California.

"Transformation Systems at NASA Ames", by Wray Buntine, Bernd Fischer, Klaus Havelund, Michael Lowry, Tom Pressburger, Steve Roach, Peter Robinson, and Jeff Van Baalen, Proceedings of Workshop on Software Transformation Systems, Los Angeles, CA, May 17th, 1999.

"Applying NASA Technology to Education, a Case Study Using Amphion", by Jane Friedman, Santos Gerardo Lazzeri, and Thomas Pressburger, Proceedings of SITE 99: Society for Information Technology and Teacher Education 10th Int'l Conf., vol. 1999, issue 1, San Antonio, TX, pp. 1918-1923, Feb. 28 to Mar. 4, 1999.

"Explaining Synthesized Software", by Jeffrey Van Baalen, Peter Robinson, Michael Lowry, Thomas Pressburger, in Proceedings 13th IEEE Conference on Automated Software Engineering, Honolulu, Hawaii, October 13-16, 1998.

"Automating Software Reuse with Amphion", by Thomas Pressburger, Michael Lowry, NASA Workshop on Software Reuse, Fairfax, VA, Sep. 24-27, 1996.

"Automated Formal Methods for Component-Based Software Development", by Michael Lowry, Thomas Pressburger, Andrew Philpot, Int'l Workshop on Formal Methods Applications, Seattle, WA, Apr. 20-22, 1995.

"Animating Observation Geometries with Amphion", by Michael Lowry, Thomas Pressburger, and Steven Roach, NASA Science Information Systems Newsletter,issue 35, pp. 35-38, Mar. 1995.

"Automatic Domain-Oriented Software Design using Formal Methods", by Pressburger, T. and Lowry M., Software Systems in Engineering, Energy-Sources Technology Conference and Exhibition, Houston, Texas, Jan. 29 - Feb. 1, 1995, pp. 33-42.

" Amphion: Specification-Based Programming for Scientific Subroutine Libraries", by Michael Lowry, Andrew Philpot, Thomas Pressburger, Ian Underwood, Proc. 3rd Int'l Symp. on Artificial Intelligence, Robotics, and Automation for Space, Pasadena, CA, pp. 41-44, Oct. 18-20, 1994

" Amphion: Automatic Programming for Scientific Subroutine Libraries", by Michael Lowry, Andrew Philpot, Thomas Pressburger, Ian Underwood, Proc. ISMIS'94: 8th Int'l Symp. on Methodologies for Intelligent Systems, Charlotte, NC, pp. 326-335, Oct. 16-19, 1994.

" A Formal Approach to Domain-Oriented Software Design Environments", by Lowry, M., Philpot, A., Pressburger, T., Underwood, I., in Proc. 9th Knowledge-Based Software Engineering Conference, Monterey, CA, Sep. 20-23, 1994, pp. 2, 48-57.

"Deductive Composition of Astronomical Software from Subroutine Libraries", by Mark Stickel, Richard Waldinger, Michael Lowry, Tom Pressburger, and Ian Underwood, Proceedings 12th International Conference on Automated Deduction (CADE-12), June 26-July 1, 1994. Lecture Notes in Artificial Intelligence, Volume 814, Springer, 1994, pp. 341-355.

"Amphion: Automatic Programming for the NAIF Toolkit", by Michael Lowry, Andrew Philpot, Thomas Pressburger, Ian Underwood, Richard Waldinger, Mark Stickel, NASA Science Information Systems Newsletter,issue 31, pp. 22-25, Feb. 1994.

"Knowledge-Based Software Development Tools", Smith, D.R. and Pressburger, T.T., in Software Engineering Environments, P. Brereton, Ed., Ellis Horwood Ltd., Chichester, 79-103, 1988.

Unpublished working papers

"Maximum Sum Subsegment Derivation" 1988 [155K, PDF]

"Squigol Exercises" 1989 [58K, PDF]

Comments and corrections to: tom.pressburger "at"
Last edited by Tom Pressburger Dec 03, 2013

Photo of Tom Pressburger


NASA Ames Research Center
Mail Stop 269-2
Moffett Field, CA 94035

Tom.Pressburger "at"

Phone: (650) 604-4878


+ RSE Homepage
+ Code TI Homepage
+ NASA Ames Homepage
+ NASA Homepage

First Gov logo
NASA Logo -