A Gallery of Verified Programs
See also
the examples
developed in Tuyen Nguyen's thesis, the ProVal
Gallery and in particular its Floating-point programs category
Short illustrative programs
Approximations of real functions
Clock drift
Infinities and not-a-number
Architecture-dependent issues