Everyone uses math libraries. Surprisingly, mainstream math libraries do not produce correct results for several thousands of inputs. Developers are seldom aware of them, which affects reproducibility and portability. We describe our new method for synthesizing elementary functions that produces correct results for all inputs but is also significantly faster than the state of the art libraries, which have been optimized for decades.
Learn how techniques from traditional compiler verification can be applied to the emerging domain of quantum computing.
Did you think test case reduction was all about debugging? Find out how test case reducers can be used for program optimisation, to generate high coverage tests, for program understanding, and even for fuzzing!
Calculating a greedy algorithm for an optimization problem, functionally.