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

DOI10.1007/978-3-030-30942-8_3zbMATH Open1539.68178MaRDI QIDQ6535939

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

Publication date: 14 March 2024

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)

Cites Work

• Title not available (Why is that?)
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• A formally verified floating-point implementation of the compact position reporting algorithm
• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
• Static Analysis of Numerical Algorithms
• Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
• Programming Languages and Systems
• Eliminating unstable tests in floating-point programs

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)