C-language floating-point proofs layered with VST and Flocq

DOI10.6092/issn.1972-5787/11442OpenAlexW3120453019MaRDI QIDQ5014364

Andrew W. Appel, Yves Bertot

Publication date: 2 December 2021

Full work available at URL: https://hal.inria.fr/hal-03130704

Mathematics Subject Classification ID

Theory of programming languages (68N15) Numerical algorithms for computer arithmetic, etc. (65Y04)

Related Items (2)

Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method ⋮ Formally-verified round-off error analysis of Runge-Kutta methods

This page was built for publication: C-language floating-point proofs layered with VST and Flocq