Provably correct floating-point implementation of a point-in-polygon algorithm

DOI10.1007/978-3-030-30942-8_3MaRDI QIDQ6535939zbMATH OpenFDO

Authors Mariano M. Moscato, Laura Titolo, Marco A. Feliú, César Muñoz

Publication date 14 March 2024

Full work available at URL https://doi.org/10.1007/978-3-030-30942-8_3

Mathematics Subject Classification ID

Numerical aspects of computer graphics, image analysis, and computational geometry (65D18) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• The point of polygon problem for arbitrary polygons
• Eliminating unstable tests in floating-point programs
• Does a point lie inside a polygon ?
• Formally certified floating-point filters for homogeneous geometric predicates
• A formally verified floating-point implementation of the compact position reporting algorithm

Cites work

• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• A formally verified floating-point implementation of the compact position reporting algorithm
• An abstract interpretation framework for the round-off error analysis of floating-point programs
• Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
• Eliminating unstable tests in floating-point programs
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• scientific article; zbMATH DE number 1863384 (Why is no real title available?)
• Programming Languages and Systems
• Static Analysis of Numerical Algorithms
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program

Cited in

(2)

• Eliminating unstable tests in floating-point programs
• Taming floating-point rounding errors with proofs (invited talk)

This page was built for publication: Provably correct floating-point implementation of a point-in-polygon algorithm

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