Gallery

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Gallery

Gallery of proved programs

Here are a few C examples of proved programs using Caduceus. They use or suffer from floating-point arithmetic.

The subtraction is exact under Sterbenz's conditions.
Malcolm's algorithm for computing the radix.
Veltkamp and Dekker algorithms for splitting a floating-point number into a lower and an upper part and for computing the error of a multiplication.
Kahan's algorithm for computing an accurate discriminant (hypothesis and proofs include the fact there is no Overflow).
A linear recurrence of order 2 has a floating-point error proportional to the square of the number of iterations (Coq proof).
François Clément's program for rope oscillation (incomplete Coq proof).