Formal verification of transcendental fixed- and floating-point algorithms using an automatic theorem prover. (English) Zbl 1522.68306
MSC:
68Q60 | Specification and verification (program logics, model checking, etc.) |
68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |