A formally verified floating-point implementation of the compact position reporting algorithm

DOI10.1007/978-3-319-95582-7_22zbMath1460.68128OpenAlexW2809379539MaRDI QIDQ2024357

César A. Muñoz, Laura Titolo, Mariano M. Moscato, François Bobot, Aaron Dutle

Publication date: 4 May 2021

Full work available at URL: http://hdl.handle.net/2060/20190002552

Mathematics Subject Classification ID

Analysis of algorithms (68W40) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35) Specification and verification (program logics, model checking, etc.) (68Q60) Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science) (68P30) Numerical algorithms for computer arithmetic, etc. (65Y04)

Related Items (1)

Formal analysis of the compact position reporting algorithm

Cites Work

• Unnamed Item
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A formal analysis of the compact position reporting algorithm
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• CC(X): Semantic Combination of Congruence Closure with Solvable Theories
• Static Analysis of Numerical Algorithms
• Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
• Programming Languages and Systems

This page was built for publication: A formally verified floating-point implementation of the compact position reporting algorithm