Sound compilation of reals

DOI10.1145/2535838.2535874zbMath1284.68393arXiv1309.2511OpenAlexW2103953062MaRDI QIDQ5408419

Viktor Kuncak, Eva Darulova

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1309.2511

zbMATH Keywords

verificationsensitivity analysisembedded systemsnumerical approximationroundoff errorcompilationscientific computingfloating-point arithmeticfixed-point arithmetic

Mathematics Subject Classification ID

Roundoff error (65G50) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

Rigorous roundoff error analysis of probabilistic floating-point computations ⋮ Bit-precise verification of discontinuity errors under fixed-point arithmetic ⋮ A two-phase approach for conditional floating-point verification ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Runtime abstract interpretation for numerical accuracy and robustness ⋮ Combining tools for optimization and analysis of floating-point computations ⋮ Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions

This page was built for publication: Sound compilation of reals