Formal analysis of the compact position reporting algorithm
DOI10.1007/s00165-019-00504-0zbMath1458.68273OpenAlexW3005752483MaRDI QIDQ1996426
Publication date: 4 March 2021
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-019-00504-0
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)
Uses Software
Cites Work
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- A formal analysis of the compact position reporting algorithm
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- A formally verified floating-point implementation of the compact position reporting algorithm
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- 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
- Programming Languages and Systems
This page was built for publication: Formal analysis of the compact position reporting algorithm
