Tom Pressburger
Computer Scientist

I work in the Robust Software Engineering Group, headed by Michael Lowry, which is in the Intelligent Systems Division (Code TI) at NASA Ames.

I have worked on software engineering technology infusion and program synthesis.

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. On sabbatical leave during the summers of 1987 and 1989, I visited Oxford, Cambridge, and Univ. of Manchester where I studied formal methods, in particular, Z, VDM, and the algebra of programming (aka Bird-Meertens "Squigol" formalism).

Experience

I lead from 2003 to 2005 the subgroup of the intercenter Software Working Group whose charter is to improve NASA's software engineering practices through research. The subgroup members were Ben Di Vito (LaRC), Martin Feather (JPL), Michael Hinchey (GSFC), Lawrence Markosian (ARC), and Luis Trevino (MSFC). Tim Menzies (West Virginia University) was also a member. The new lead is Wes Deadrick of the NASA IV&V Facility. The subgroup is involved in selecting mature software engineering research technologies and starting pilot projects making use of them in NASA software development efforts. See Research Infusion. The subgroup was awarded "Best New Research" at NASA OSMA SAS'04.

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

• Amphion: solar system geometry;
• AutoBayes: statistical analysis;
• Amphion/NAV (a precursor to AutoFilter): state estimation using Kalman filters;
• 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 can efficiently process it (such hand-tuning will eventually be 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 reengineering platform Software Refinery (TM) provided by Reasoning, Inc. (now defunct) and used it to analyze and transform COBOL programs.

Professional Memberships

• ACM
• IEEE Computer Society

Service

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

Reviewer for the Automated Sofware Engineering journal.

Publications

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

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

"Squigol Exercises" 1989 [58K, PDF]

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

Comments and corrections to: tom.pressburger "at" nasa.gov (Tom Pressburger)

Principal Investigator, Robust Software Engineering group: michael.r.lowry "at" nasa.gov (Michael Lowry)