Susan Gerhart

{{Infobox scientist | name = Susan L. Gerhart | image = | caption = | birth_date = | birth_place = | nationality = American | fields = Computer science, software engineering, formal methods, software verification | alma_mater = Ohio Wesleyan University, Carnegie Mellon University | doctoral_advisor = Mary Shaw | known_for = Formal methods for software verification, Gypsy system, pioneering work in software engineering | awards = IEEE Computer Society Harlan D. Mills Award (2007) }}

Susan L. Gerhart is an American computer scientist renowned for her pioneering work in formal methods for software verification and her significant contributions to the field of software engineering. She is particularly recognized for her role in the development of the Gypsy verification system, one of the earliest and most influential systems to apply rigorous mathematical techniques to ensure the correctness and reliability of software.

Early Life and Education

Gerhart earned her Bachelor of Arts degree in mathematics from Ohio Wesleyan University. She continued her academic pursuits in computer science, receiving her Master of Science and Doctor of Philosophy degrees from Carnegie Mellon University. Her doctoral research, supervised by Mary Shaw, focused on program verification and laid the groundwork for her subsequent career in formal methods.

Career and Contributions

Gerhart's career has encompassed roles in academia, industry research, and government service, consistently focusing on improving the quality and reliability of software through rigorous methods.

Formal Methods and the Gypsy System

A central theme of Gerhart's research has been the application of formal methods—mathematically based techniques for the specification, development, and verification of software and hardware systems. In the late 1970s, while at the University of Texas at Austin and later at the Information Sciences Institute (ISI) of the University of Southern California (USC), she was a key contributor to the development of the Gypsy verification system. Gypsy was a groundbreaking system that integrated a programming language with formal specification and verification tools, allowing developers to mathematically prove properties of their software. This work was instrumental in demonstrating the practical feasibility of using formal methods for critical systems, especially for high-assurance and secure operating systems, influencing subsequent research and development in secure computing.

Other Professional Roles

Throughout her distinguished career, Gerhart has held several influential positions:

Academia: She held faculty positions, including at the University of Texas at Austin, where she conducted foundational research in program verification.
Industry Research: She worked at the Microelectronics and Computer Technology Corporation (MCC) in the 1980s, continuing her research in software engineering, reusability, and software architectures.
Government Service: Gerhart served as a program director at the National Science Foundation (NSF), where she played a role in shaping research funding and strategic directions in software engineering and related computing fields.

Her work has profoundly impacted software engineering by advocating for and demonstrating the practical value of mathematically sound approaches to software development, thereby contributing to the maturity and trustworthiness of software systems. She has authored numerous influential papers on program verification, formal methods, software reliability, and software reusability.

Awards and Recognition

In recognition of her foundational contributions to software engineering and formal methods, Susan Gerhart was awarded the [[IEEE Computer Society Harlan D. Mills Award]] in 2007. The award citation specifically honored her "contributions to the application of formal methods in software engineering, especially for her leadership in the development and demonstration of the Gypsy verification environment."

Selected Publications

Gerhart, S. L. (1975). Correctness-Preserving Program Transformations. Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 165-174.
Good, D. I., London, R. L., & Gerhart, S. L. (1979). An interactive program verification system. IEEE Transactions on Software Engineering, (1), 59-67.
Gerhart, S. L. (1987). Formal methods: the next stage of development. IEEE Transactions on Software Engineering, (2), 263-268.

Find the meaning, context, and related topics in one search.