Open Access 2022 | OriginalPaper | Buchkapitel
Inferring Interval-Valued Floating-Point Preconditions
verfasst von : Jonas Krämer, Lionel Blatter, Eva Darulova, Mattias Ulbrich
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Aggregated roundoff errors caused by floating-point arithmetic can make numerical code highly unreliable. Verified postconditions for floating-point functions can guarantee the accuracy of their results under specific preconditions on the function inputs, but how to systematically find an adequate precondition for a desired error bound has not been explored so far. We present two novel techniques for automatically synthesizing preconditions for floating-point functions that guarantee that user-provided accuracy requirements are satisfied. Our evaluation on a standard benchmark set shows that our approaches are complementary and able to find accurate preconditions in reasonable time.