Formal analysis of the compact position reporting algorithm

DOI10.1007/s00165-019-00504-0zbMath1458.68273OpenAlexW3005752483MaRDI QIDQ1996426

Yanyan Li

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

zbMATH Keywords

formal analysisPVSFrama-Ccompact position reporting algorithmfinite precision computation

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)

Uses Software

• PVS
• ACSL
• Frama-C
• Gappa
• cvc3
• z3
• ASTREE
• PRECiSA

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