Using PVS to validate the algorithms of an exact arithmetic.

DOI10.1016/S0304-3975(02)00226-8MaRDI QIDQ1853641zbMATH OpenFDO

Authors 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)

Recommendations

• The world's shortest correct exact real arithmetic program?
• Real Number Calculations and Theorem Proving
• Numerical Software with Result Verification
• Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
• Affine arithmetic and applications to real-number proving

Cites work

• scientific article; zbMATH DE number 3987247 (Why is no real title available?)
• scientific article; zbMATH DE number 4023258 (Why is no real title available?)
• scientific article; zbMATH DE number 42077 (Why is no real title available?)
• scientific article; zbMATH DE number 3066801 (Why is no real title available?)
• Nicht konstruktiv beweisbare Sätze der Analysis
• On computable sequences
• On the definitions of some complexity classes of real numbers
• Recursive Real Numbers

Cited in

(8)

• Numerical Software with Result Verification
• Real Number Calculations and Theorem Proving
• Robustness and Randomness
• Abstract State Machines with Exact Real Arithmetic
• Arbitrary precision real arithmetic: design and algorithms
• The world's shortest correct exact real arithmetic program?
• Affine arithmetic and applications to real-number proving
• scientific article; zbMATH DE number 1746032 (Why is no real title available?)

Describes a project that uses

Uses Software

• PVS

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1853641)