Title: Formal Methods Seminar: Solving Mixed Real and Floating-Point Formulas
Speaker: Rocco Salvia (University of Utah, PhD Student), NIA Visitor
Date: Friday, December 7, 2018
Time: 10:30am – 12:00pm
Location: NASA/LaRC, Bldg. 1230, Room 264A
Host: Cesar A. Munoz, NASA/LaRC
Abstract: Reasoning about mixed real and floating-point arithmetic is essential for modeling round-off errors and for developing accurate analysis tools for floating-point programs. In this talk, we present FPRoCk, a prototype tool for solving mixed real and floating-point formulas. FPRoCk transforms a mixed formula into an equi-satisfiable one over the reals. This transformed formula is then input to different off-the-shelf SMT solvers with support for real arithmetic. The proposed tool is integrated inside the static analyzer PRECiSA, which computes a sound estimation of the round-off error of floating-point programs. In particular, FPRoCk is used to detect unfeasible computational paths to improve the accuracy of PRECiSA.
Bio: Rocco Salvia is a PhD student at the School of Computing at the University of Utah. He works at the SOARlab research group, headed by Zvonimir Rakamaric. Before joining SOARlab, he graduated in Computer Science at University of Venice, Italy under the supervision of Agostino Cortesi. Upon graduating he became employed at Julia in Verona, Italy where he primarily worked on static analysis of Java bytecode through abstract interpretation. At present, his research interest is about approximate computing applied to machine learning predictors, but also what the effects of floating-point arithmetic are on the correctness of computer programs.