Sökning: id:"swepub:oai:research.chalmers.se:28d088a5-ecd7-4bbd-9b0c-73b418c719c6" >
A Verified Certific...
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
-
Becker, Heiko (författare)
-
Zyuzin, Nikita (författare)
-
- Monat, Raphael (författare)
- École Normale Supérieure de Lyon
-
visa fler...
-
Darulova, Eva (författare)
-
- Myreen, Magnus, 1983 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Fox, Anthony C. J. (författare)
- University Of Cambridge
-
visa färre...
-
(creator_code:org_t)
- 2018
- 2018
- Engelska.
-
Ingår i: Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018. ; , s. 215-224
- Relaterad länk:
-
https://doi.org/10.2...
-
visa fler...
-
https://research.cha...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- Being able to soundly estimate roundoff errors of finite-precision computations is important for many applications in embedded systems and scientific computing. Due to the discrepancy between continuous reals and discrete finite-precision values, automated static analysis tools are highly valuable to estimate roundoff errors. The results, however, are only as correct as the implementations of the static analysis tools. This paper presents a formally verified and modular tool which fully automatically checks the correctness of finite-precision roundoff error bounds encoded in a certificate. We present implementations of certificate generation and checking for both Coq and HOL4 and evaluate it on a number of examples from the literature. The experiments use both in-logic evaluation of Coq and HOL4, and execution of extracted code outside of the logics: we benchmark Coq extracted unverified OCaml code and a CakeML-generated verified binary.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Reglerteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Control Engineering (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Medicinteknik -- Medicinsk bildbehandling (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Medical Engineering -- Medical Image Processing (hsv//eng)
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)