Formal analysis of the compact position reporting algorithm

DOI10.1007/S00165-019-00504-0MaRDI QIDQ1996426zbMATH OpenOpenAlexFDO

Authors 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

compact position reporting algorithmfinite precision computationformal analysisFrama-CPVS

Mathematics Subject Classification ID

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

Recommendations

• A formal analysis of the compact position reporting algorithm
• A formally verified floating-point implementation of the compact position reporting algorithm
• Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm
• scientific article; zbMATH DE number 1852171
• scientific article; zbMATH DE number 1670737

Cites work

• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• A formal analysis of the compact position reporting algorithm
• A formally verified floating-point implementation of the compact position reporting algorithm
• An abstract interpretation framework for the round-off error analysis of floating-point programs
• Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
• Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Programming Languages and Systems
• Programming Languages and Systems
• Static Analysis of Numerical Algorithms
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program

Cited in

(5)

• A formal analysis of the compact position reporting algorithm
• A formally verified floating-point implementation of the compact position reporting algorithm
• scientific article; zbMATH DE number 1670737 (Why is no real title available?)
• Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm
• Embedding differential dynamic logic in PVS

Describes a project that uses

Uses Software

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

This page was built for publication: Formal analysis of the compact position reporting algorithm

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1996426)