Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function. - Paul Bonnot; Benoît Boyer; Florian Faissole; Claude Marché; Raphaël Rieu-Helft (FMCAD, 2024)