Loop invariants in floating point algorithms

DOI10.1007/BF02243815MaRDI QIDQ685861zbMATH OpenFDO

Authors K.-U. Jahn

Publication date 18 October 1993

Published in Computing (Search for Journal in Brave)

zbMATH Keywords

numerical algorithmsloop invariantsrounding errorsdirecting roundingsenclosure setsfloating point algorithmloop conditionsresult verification

Mathematics Subject Classification ID

Roundoff error (65G50) Specification and verification (program logics, model checking, etc.) (68Q60) Interval and finite arithmetic (65G30)

Recommendations

• Counterexample- and simulation-guided floating-point loop invariant synthesis
• FM 2005: Formal Methods
• Accurate and efficient algorithms for floating point computation
• Programming Languages and Systems
• Algorithms for efficient reproducible floating point summation
• Floating-point error propagation in iterative methods
• An iterative method for generating loop invariants
• Faithfully rounded floating-point computations
• Publication:3033331

Cites work

• scientific article; zbMATH DE number 3874497 (Why is no real title available?)
• scientific article; zbMATH DE number 3880009 (Why is no real title available?)
• scientific article; zbMATH DE number 3905740 (Why is no real title available?)
• scientific article; zbMATH DE number 4047034 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3766957 (Why is no real title available?)
• scientific article; zbMATH DE number 44308 (Why is no real title available?)
• scientific article; zbMATH DE number 67122 (Why is no real title available?)
• scientific article; zbMATH DE number 3502707 (Why is no real title available?)
• scientific article; zbMATH DE number 3300589 (Why is no real title available?)
• An axiomatic basis for computer programming
• Basic results for the behaviour of discrete iterations
• Evaluation of Hausdorff distances in interval mathematics
• Punktkonvergenz in der Intervall‐Rechnung
• Über die Notwendigkeit einer Fehlerschranken-Arithmetik für Rechenautomaten

Cited in

(2)

• New tools for localization of limit cycles in recursive block floating point systems
• Counterexample- and simulation-guided floating-point loop invariant synthesis

This page was built for publication: Loop invariants in floating point algorithms

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