A formally verified floating-point implementation of the compact position reporting algorithm
type: Item
instance of: scholarly article
title: A formally verified floating-point implementation of the compact position reporting algorithm
zbMATH Open document ID: 1460.68128
DOI: 10.1007/978-3-319-95582-7_22
author: Laura Titolo
author: Mariano M. Moscato
author: César Muñoz
author: Aaron Dutle
author: François Bobot
publication date: 2021-05-04T00:00:00Z
full work available at URL: http://hdl.handle.net/2060/20190002552
Mathematics Subject Classification ID: 68U35
Mathematics Subject Classification ID: 65Y04
Mathematics Subject Classification ID: 68P30
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68W40
zbMATH DE Number: 7343222
MaRDI profile type: Publication
OpenAlex ID: W2809379539
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Wave equation numerical resolution: a comprehensive mechanized proof of a C program
cites work: Formal verification of numerical programs: from C annotated programs to mechanical proofs
cites work: \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
cites work: Q4414726
cites work: Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
cites work: A formal analysis of the compact position reporting algorithm
cites work: Static Analysis of Numerical Algorithms
cites work: Programming Languages and Systems
Recommended article: A formal analysis of the compact position reporting algorithm
Recommended article: Formal analysis of the compact position reporting algorithm
Recommended article: Formal Verification of Floating-Point Hardware Design
Recommended article: Verified compilation of floating-point computations
Recommended article: Formal verification of a floating-point expansion renormalization algorithm
Recommended article: Formal verification of the VAMP floating point unit
Recommended article: Q4787242
Recommended article: Verification methods: rigorous results using floating-point arithmetic
Recommended article: Correct approximation of IEEE 754 floating-point arithmetic for program verification
description: scientific article; zbMATH DE number 7343222