Formal analysis of the compact position reporting algorithm
type: Item
instance of: scholarly article
title: Formal analysis of the compact position reporting algorithm
zbMATH Open document ID: 1458.68273
author: Yanyan Li
published in: Formal Aspects of Computing
publication date: 2021-03-04T00:00:00Z
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: 7317637
zbMATH Keywords: formal analysis
zbMATH Keywords: finite precision computation
zbMATH Keywords: compact position reporting algorithm
zbMATH Keywords: Frama-C
zbMATH Keywords: PVS
describes a project that uses: ACSL
describes a project that uses: cvc3
describes a project that uses: ASTREE
describes a project that uses: PRECiSA
describes a project that uses: Gappa
describes a project that uses: PVS
describes a project that uses: z3
describes a project that uses: Frama-C
MaRDI profile type: Publication
full work available at URL: s00165-019-00504-0
OpenAlex ID: W3005752483
cites work: Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
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: Programming Languages and Systems
cites work: \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
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: An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
cites work: A formally verified floating-point implementation of the compact position reporting algorithm
DOI: 10.1007/S00165-019-00504-0
description: scientific article; zbMATH DE number 7317637