Come and enjoy a lunch & learn Technical Seminar hosted by the AIAA Hampton Roads Section at the NASA Langley Research Center. This lunch and learn will be offered on site in the Pearl Young Theater but also virtually for our colleagues who are not local to the area. Here are the details for this month's talk.
RSVP: Google Form Registration - Titolo
Title: Taming numerical errors in safety-critical avionics applications
Presenter: Dr. Laura Titolo
Abstract: The development of software that depends on floating-point computations is particularly challenging due to the presence of round-off errors in computer arithmetic. These errors accumulate during numerical computations and may significantly affect the evaluation of both arithmetic and Boolean expressions. Reasoning on floating-point computations is particularly important for safety-critical software where the divergence between the ideal real number computation and its floating-point counterpart can lead to catastrophic consequences. This talk provides an overview of the different formal methods techniques that have been implemented and integrated to analyze numerical properties of NASA libraries for avionics applications such as geofencing, detect-and-avoid, and aircraft positioning. Employed techniques include abstract interpretation, theorem proving, SMT solvers, and numerical methods which have been successfully integrated to improve floating-point programs and to provide formal guarantees of their correctness.
BIO: Laura Titolo is a Senior Research Scientist at the National Institute of Aerospace working in the Safety-Critical Avionics Systems Branch at NASA Langley Research Center. She received her Ph.D. in Computer Science from the University of Udine (Italy) in 2014. Previously, she earned a Bachelor's and a Master's degree in Computer Science from the University of Udine. Before joining NIA in 2015, Laura was a post-doctoral researcher at the University of Malaga (Spain). Her research interests include several aspects of programming languages and formal methods. In particular, she works on developing new techniques and tools for the formal verification and analysis of safety-critical avionics applications.
------------------------------
Matthew Galles
NASA Langley Research Center
Hampton VA
matthew.b.galles@nasa.gov------------------------------