×
Dutle, Aaron; Moscato, Mariano; Titolo, Laura; Muñoz, César; Anderson, Gregory; Bobot, François

Formal analysis of the compact position reporting algorithm. (English) Zbl 1458.68273

Formal Asp. Comput. 33, No. 1, 65-86 (2021).

MSC:

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

Keywords:

formal analysis; finite precision computation; compact position reporting algorithm; Frama-C; PVS

Software:

z3; Frama-C; ACSL; PVS; ASTREE; cvc3; PRECiSA; Gappa
Cite Review PDF
Full Text: DOI

References:

[1] Barrett C, Tinelli C (2007) CVC3. In: Proceedings of the 19th international conference on computer aided verification, CAV 2007, pp 298-302 · Zbl 1119.68005
[2] Bouissou O, Conquet E, Cousot P, Cousot R, Feret J, Goubault E, Ghorbal K, Lesens D, Mauborgne L, Miné A, Putot S, Rival X, Turin M (2009) Space software validation using abstract interpretation. In: Proceedings of the international space system engineering conference, data systems in aerospace (DASIA 2009). ESA Publications, pp 1-7
[3] Bertrane, J.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Rival, X., Static analysis and verification of aerospace software by abstract interpretation, Found Trends Program Lang., 2, 2-3, 71-190 (2015) · doi:10.1561/2500000002
[4] Boldo, S.; Clément, F.; Filliâtre, JC; Mayero, M.; Melquiond, G.; Weis, P., Wave equation numerical resolution: a comprehensive mechanized proof of a C program, J. Autom Reason, 50, 4, 423-456 (2013) · Zbl 1267.68208 · doi:10.1007/s10817-012-9255-4
[5] Baudin P, Cuoq P, Filliâtre JC, Marché C, Monate B, Moy Y, Prevosto V (2016) ACSL: ANSI/ISO C Specification Language, version 1.12
[6] Bobot, F.; Filliâtre, JC; Marché, C.; Paskevich, A., Let’s verify this with Why3, Int J Softw Tools Technol Transf, 17, 6, 709-727 (2015) · doi:10.1007/s10009-014-0314-5
[7] Boldo, S.; Marché, C., Formal verification of numerical programs: from C annotated programs to mechanical proofs, Math Comput Sci, 5, 4, 377-393 (2011) · Zbl 1264.68054 · doi:10.1007/s11786-011-0099-9
[8] Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977. ACM, pp 238-252
[9] Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival (2005) The ASTREÉ analyzer. In: Proceedings of the 14th European Symposium on Programming (ESOP 2005), vol 3444 of lecture notes in computer science. Springer, Berlin, pp 21-30 · Zbl 1108.68422
[10] Conchon, S.; Contejean, E.; Kanig, J.; Lescuyer, S., CC(X): semantic combination of congruence closure with solvable theories, Electron Notes Theor Comput Sci, 198, 2, 51-69 (2008) · Zbl 1277.68240 · doi:10.1016/j.entcs.2008.04.080
[11] Chen L, Miné A, Cousot P (2008) A sound floating-point polyhedra abstract domain. In: Proceedings of the 6th Asian symposium on programming languages and systems, APLAS 2008, vol 5356 of lecture notes in computer science. Springer, Berlin, pp 3-18
[12] Code of Federal Regulations (2015) Automatic dependent surveillance-broadcast (ADS-B) out, 91 c.f.r., section 225
[13] de Dinechin, F.; Lauter, C.; Melquiond, G., Certifying the floating-point implementation of an elementary function using Gappa, IEEE Trans Comput, 60, 2, 242-253 (2011) · Zbl 1367.65250 · doi:10.1109/TC.2010.128
[14] de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2008, vol 4963 of lecture notes in computer science. Springer, Berlin, pp 337-340
[15] Dutle A, Moscato M, Titolo L, Muñoz C (2017) A formal analysis of the compact position reporting algorithm. In: 9th Working conference on verified software: theories, tools, and experiments, VSTTE 2017, revised selected papers, vol 10712, pp 19-34 · Zbl 1403.68324
[16] Delmas D, Souyris J (2007) Astrée: from research to industry. In: Proceedings of the 14th international symposium on static analysis, SAS, pp 437-451
[17] European Commission (2017) Commission implementing regulation (EU) 2017/386 of 6 march 2017 amending implementing regulation (EU) No 1207/2011, C/2017/1426, 2017
[18] Goodloe A, Muñoz C, Kirchner F, Correnson L (2013) Verification of numerical programs: from real numbers to floating point numbers. In: Proceedings of NFM 2013, vol. 7871 of lecture notes in computer science. Springer, Berlin, pp 441-446
[19] Goubault E, Putot S (2006) Static analysis of numerical algorithms. In: Proceedings of SAS 2006, vol 4134 of lecture notes in computer science. Springer, Berlin, pp 18-34 · Zbl 1225.68073
[20] Kirchner, F.; Kosmatov, N.; Prevosto, V.; Signoles, J.; Yakobowski, B., Frama-C: a software analysis perspective, Formal Aspects Comput, 27, 3, 573-609 (2015) · doi:10.1007/s00165-014-0326-7
[21] Marché, C., Verification of the functional behavior of a floating-point program: an industrial case study, Sci Comput Program, 96, 279-296 (2014) · doi:10.1016/j.scico.2014.04.003
[22] Miné A (2004) Relational abstract domains for the detection of floating-point run-time errors. In: Proceedings of the 13th European symposium on programming languages and systems, ESOP 2004, vol 2986 of lecture notes in computer science. Springer, Berlin, pp 3-17 · Zbl 1126.68353
[23] Marché C, Moy Y (2017) The Jessie Plugin for deductive verification in Frama-C
[24] Moscato MM, Titolo L, Dutle A, Muñoz C (2017) Automatic estimation of verified floating-point round-off errors via static analysis. In: Proceedings of the 36th international conference on computer safety, reliablilty, and security, SAFECOMP 2017 · Zbl 1403.68324
[25] Moscato MM, Titolo L, Feliú MA, Muñoz CA (2019) Provably correct floating-point implementation of a point-in-polygon algorithm. In: Proceedings of the third World congress on formal methods-the next 30 years (FM 2019), vol 11800 of lecture notes in computer science. Springer, Berlin, pp 21-37 · Zbl 1539.68178
[26] Owre S, Rushby J, Shankar N (1992) PVS: a prototype verification system. In: Proceedings of CADE 1992, vol 607 of lecture notes in artificial intelligence. Springer, Berlin, pp 748-752
[27] RTCA SC-186 (2009) Minimum operational performance standards for 1090 MHz extended squitter automatic dependent surveillance-broadcast (ADS-B) and traffic information services-broadcast (TIS-B)
[28] Titolo L, Feliú M, Moscato M, Muñoz C (2018) An abstract interpretation framework for the round-off error analysis of floating-point programs. In: Proceedings of the 19th international conference on verification, model checking, and abstract interpretation, VMCAI 2018, vol 10747. Springer, Berlin, pp 516-537 · Zbl 1446.68036
[29] Titolo L, Moscato MM, Muñoz CA, Dutle A, Bobot F (2018) A formally verified floating-point implementation of the compact position reporting algorithm. In: Proceedings of the 22nd international symposium on formal methods (FM 2018), vol 10951 of lecture notes in computer science. Springer, Berlin, pp 364-381 · Zbl 1460.68128
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.