Congratulations to Prof. Santosh Nagarakatte, who has just received an NSF grant for his project titled "SHF:Small: Formalisms, Implementations, and Verification Procedures for Alternatives to Floating-Point", for an amount of $500,000, covering a three-year period starting 07/01/2019. He is the sole investigator on the project.

Efficient and accurate representation of real numbers is a foundational question in computer science. A floating-point number is widely used to approximate a real number using a finite number of bits. Given the need for good performance and challenges in reasoning about rounding errors or exceptional conditions with the floating-point representation, there is interest in the community to explore possible alternatives to it. The Posit representation is a recently proposed alternative to the IEEE-754 floating point representation. The Posit representation can represent more real numbers than the floating-point representation given the same number of bits. Depending on the configuration, it can represent every real value that floating point can. The Posit community is attempting to find specific applications where a Posit outperforms floating point in accuracy, performance, or storage.

This project develops techniques, tools, and procedures to determine whether Posit is a viable alternative to floating point. This project's impacts are the following: (1) enable programmers to effectively write correct programs using Posits, (2) make foundational advances for generating high-performance math libraries and automated reasoning for Posits, (3) influence domain experts in scientific computing and alleviate their concerns about correctness and accuracy, and (4) educate graduate, undergraduate, and high-school students on foundational abstractions and reasoning techniques.To reason about the accuracy of computation, the project develops technique for fast shadow execution that compares a Posit execution to an execution with real numbers. To enable automated reasoning for programs using Posits, the project develops a theory of Posits usable with satisfiability modulo theory solvers.

More details can be found on National Science Foundation's webpage