Lauren M. White

Dr. Lauren M. White works in the Formal Methods Research team, a part of NASA Langley's Safety-Critical Avionics Systems Branch, developing formal methods tools to aid in the formal verification process of safety-critical avionics systems of interest to NASA. Her research interests include the application of mathematical concepts and formal logic in solving real-world problems. In her work with NASA, Dr. White has contributed to the NASA library for the interactive theorem prover the Prototype Verification System (PVS). This work includes the embedding of differential dynamic logic in PVS, called Plaidypvs.

Dr. White also serves as a team lead in the Convergent Aeronautics Solutions (CAS) project as part of their Discovery effort. The goal of the CAS project is to explore seemly improbable ideas that might lead to solutions to the problems that plague aviation and impact safety, environmental and community impact, and the global growth in air traffic. Dr. White and her Discovery team were tasked to rapidly assess the feasibility of concepts that utilized NASA capabilities to address the unique challenges faced by rural America.

Dr. White received her PhD in mathematics from Kansas State University as a student of Anna Zemlyanova studying nanoscale contact mechanics.

Publications

• Frankforter E., Bowes A., Brubaker E., Logan M., Miller A., Stancliff M., White L. M., Rask J., Fuller D., Bond K., Knight A. (2025). Convergent Opportunities in Unmanned Aircraft Systems for Civil and Aerospace Inspection. In Proceedings of AIAA Aviation 2025.
• Logan M., White L. M., Bowes A., Frankforter E., Brubaker E., Miller A., Stancliff M., Rask J., Fuller D., Knight A., Bond K. (2025). Applications of UAS Technologies to Create Resilient Rural Communities. In Proceedings of AIAA Aviation 2025.
• Knight A., White L. M., Rask J., Bond K., Bowes A., Frankforter E., Fuller D., Logan M., Stancliff M., Miller A., Brubaker E. (2025). Design Logic Visualizations as boundary objects in design. In Proceedings of the International Conference on Engineering Design (ICED) 2025.
• Slagel, J. T., Dutle, A., White, L. M., Muñoz, C., & Crespo, N. (2024). A Verification Framework for Runtime Assurance of Autonomous UAS. In proceedings of the 43rd Digital Avionics Systems Conference (DASC).
• Slagel, J. T., Dutle, A., White, L. M., & Muñoz, C., & Crespo, N. (2024). A Formal Verification Framework for Runtime Assurance. In proceedings of the NASA Formal Methods Conference 2024.
• White, L. M., Titolo, L., Slagel, J. T., & Muñoz, C. (2024). A Temporal Differential Dynamic Logic Formal Embedding. In proceedings of the International Conference on Certified Programs and Proofs 2024.
• Slagel, J. T., Moscato, M., White, L. M., Muñoz, C., Balachandran, S., & Dutle, A. (2023). Embedding Differential Dynamic Logic in PVS. In Proceedings of the 18th International Workshop on Logical and Semantic Frameworks, with Applications.
• White, L. M., Titolo, L., & Slagel, J. T. (2023). Embedding Differential Temporal Dynamic Logic in PVS. In 29th International Conference on Types for Proofs and Programs TYPES 2023 Abstracts (p. 92).
• Slagel, J. T., Moscato, M., White, L. M., Muñoz, C., Balachandran, S., & Dutle, A. (2023). Embedding Differential Dynamic Logic in PVS. In Proceedings of the 18th International Workshop on Logical and Semantic Frameworks, with Applications.
• Zemlyanova, A. Y., & White, L. M. (2023). An axisymmetric problem for a patch loaded membrane attached to the surface of an elastic semi-space. SIAM Journal on Applied Mathematics 83.2 (2023): 603-624.
• Slagel, J. T., Muñoz, C., Balachandran, S., Moscato, M., Dutle, A., Masci, P., & White, L. (2022). Towards an implementation of differential dynamic logic in PVS. In Proceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (pp. 44-50).
• Zemlyanova, A. Y., & White, L. M. (2022). Axisymmetric frictionless indentation of a rigid stamp into a semi-space with a surface energetic boundary. Mathematics and Mechanics of Solids, 27(2), 334-347.
• Slagel, J. T., White, L., & Dutle, A. (2021). Formal verification of semi-algebraic sets and real analytic functions. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 278-290).
• Cowan, R. A., Katz, D. J., & White, L. M. (2017). A new generating function for calculating the Igusa local zeta function. Advances in Mathematics, 304, 355-420.