Formal Verification of the Pentium ® 4 Floating-Point Multiplier.

Roope Kaivola Naren Narasimhan

Published in: DATE (2002)

Keyphrases

floating point
formal verification
model checking
fixed point
square root
automated verification
model checker
instruction set
bounded model checking
sparse matrices
symbolic model checking
program slicing
floating point arithmetic
image segmentation
dynamic programming
interval arithmetic