Using PVS to validate the algorithms of an exact arithmetic.

DOI10.1016/S0304-3975(02)00226-8zbMath1064.68005MaRDI QIDQ1853641

Paul Gowland, David R. Lester

Publication date: 21 January 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

Cauchy sequencesPVSCorrectnessExact arithmeticComputable reals

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07)

Related Items (5)

Abstract State Machines with Exact Real Arithmetic ⋮ Robustness and Randomness ⋮ Real Number Calculations and Theorem Proving ⋮ The world's shortest correct exact real arithmetic program? ⋮ Arbitrary precision real arithmetic: design and algorithms

Uses Software

• PVS

Cites Work

• On computable sequences
• On the definitions of some complexity classes of real numbers
• Nicht konstruktiv beweisbare Sätze der Analysis
• Recursive Real Numbers
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Using PVS to validate the algorithms of an exact arithmetic.