Title: A Formalization of Analytical Solutions for Cubic Polynomials in PVS
Speaker: Nabil Kherraf, Ecole Normale Superieure de Lyon, NIA Visitor
Location: NASA/LaRC, B1230 R264A
Time: 10:30 AM – 12:00 PM September 6, 2018
Sponsor: Cesar Munoz, NASA/LaRC
Abstract: Finding roots of cubic and quartic polynomials plays a fundamental role in separation assurance systems where aircraft trajectories are represented by low degree polynomials. This talk presents a formalization in the Prototype Verification System (PVS) of a method to analytically find roots of cubic polynomials. The presentation will cover the theoretical approach based in the well-known reduction of the problem of finding roots of a cubic polynomial into solving a quadratic polynomial through the so-called Vieta’s Substitution. Highlights of the formalization will be presented as well as pointing out technical problems and proposed solutions for its PVS implementation. Known approaches to deal with quartic polynomials will also be discussed, along with a brief feasibility study of its formalization in PVS.
Bio: Nabil Kherraf is a graduate student in Theoretical Computer Science at Ecole Normale Superieure de Lyon, France. He holds a BSc. in Mathematics & Computer Science from University of Montpellier, France. This work has been conducted as part of a 10-weeks visit at the National Institute of Aerospace supporting NASA’s System Wide Safety project.