naa a22 4500 510791263 CHVBK 20180411083320.0 cr unu---uuuuu 180411e20130601xx s 000 0 eng 10.1007/s11334-013-0195-x doi (NATIONALLICENCE)springer-10.1007/s11334-013-0195-x Affeldt Reynald National Institute of Advanced Industrial Science and Technology, Central 2, 1-1-1, Umezono, Tsukuba, Ibaraki, Japan aut On construction of a library of formally verified low-level arithmetic functions [Elektronische Daten] [Reynald Affeldt] Arithmetic functions are used in many important computer programs such as computer algebra systems and cryptographic software. The latter are critical applications whose correct implementation deserves to be formally guaranteed. They are also computation-intensive applications, so that programmers often resort to low-level assembly code to implement arithmetic functions. We propose an approach for the construction of a library of formally verified low-level arithmetic functions. To build our library, we first introduce a formalization of data structures for signed multi-precision arithmetic in low-level programs. We use this formalization to verify the implementation of several primitive arithmetic functions using Separation logic, an extension of Hoare logic to deal with pointers. Since this direct style of formal verification leads to technically involved specifications, we also propose for larger functions to show a formal simulation relation between pseudo-code and assembly. This style of verification is illustrated with a concrete implementation of the binary extended gcd algorithm. Springer-Verlag London, 2013 Proof-assistant nationallicence Coq nationallicence Hoare logic nationallicence Separation logic nationallicence Assembly programming language nationallicence Multi-precision arithmetic nationallicence Simulation nationallicence Innovations in Systems and Software Engineering Springer-Verlag 9/2(2013-06-01), 59-77 1614-5046 9:2<59 2013 9 11334 https://doi.org/10.1007/s11334-013-0195-x text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s11334-013-0195-x text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Affeldt Reynald National Institute of Advanced Industrial Science and Technology, Central 2, 1-1-1, Umezono, Tsukuba, Ibaraki, Japan aut NATIONALLICENCE 773 0- Innovations in Systems and Software Engineering Springer-Verlag 9/2(2013-06-01), 59-77 1614-5046 9:2<59 2013 9 11334 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer