Proof engineering in the large: formal verification of Pentium?4 floating-point divider.
Roope KaivolaKatherine R. KohatsuPublished in: Int. J. Softw. Tools Technol. Transf. (2003)
Keyphrases
- floating point
- formal verification
- model checking
- bounded model checking
- fixed point
- model checker
- square root
- symbolic model checking
- software engineering
- sparse matrices
- program slicing
- automated verification
- instruction set
- floating point arithmetic
- artificial intelligence
- interval arithmetic
- computer science
- theorem proving
- theorem prover
- pairwise
- probabilistic model