Using PVS to validate the algorithms of an exact arithmetic.

DOI10.1016/S0304-3975(02)00226-8zbMATH Open1064.68005MaRDI QIDQ1853641FDOQ1853641

Authors: Paul Gowland, David R. Lester 

Publication date: 21 January 2003

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

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

zbMATH Keywords

Cauchy sequencesPVSCorrectnessExact arithmeticComputable reals

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07)

Cites Work

• Title not available (Why is that?)
• Nicht konstruktiv beweisbare Sätze der Analysis
• Title not available (Why is that?)
• Recursive Real Numbers
• On the definitions of some complexity classes of real numbers
• Title not available (Why is that?)
• On computable sequences
• Title not available (Why is that?)

Cited In (8)

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

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)