Floating Point and Linear Algebra

Todo: Write up ideas for smooth integration of floating point in Whiley without complicating the verifier. See forum thread on modelling unknown bits.

Resources

IEEE 754-2008 (pdf)

Intel instruction manual (pdf)

AMD instructions (pdf)

Floating point bit-explorer tool (online javascript app)

How the Intel compiler deals with floating point optimization (pdf)

Intel intrinsics guide (online browser)

Instruction performance on various CPUs: cycles, throughput (pdf)

Papers on verification:

Invariant and Type Inference for Matrices? (pdf, VMCAI2010)