Iterators: where folds fail

Sylvie Boldo (1)

1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations

This paper is about the formal verification of a floating-point case study where the common iterators fold_left and fold_right have not the wanted behaviors. We then had to define other iterators, which are very similar in most cases, but that do behave well in our case study.

Domaines: Logique en informatique [cs.LO]

Sylvie Boldo. Iterators: where folds fail. Workshop on High-Consequence Control Verification, Jul 2016, Toronto, Canada. ⟨hal-01377155⟩