Zobrazeno 1 - 5
of 5
pro vyhledávání: '"Raphaël Rieu-Helft"'
Publikováno v:
ISSAC'20: Proceedings of the 45th International Symposium on Symbolic and Algebraic Computation
ISSAC 2020: 45th International Symposium on Symbolic and Algebraic Computation
ISSAC 2020: 45th International Symposium on Symbolic and Algebraic Computation, Jul 2020, Kalamata, Greece
Journal of Symbolic Computation
Journal of Symbolic Computation, 2023, 115, pp.74-95. ⟨10.1016/j.jsc.2022.07.007⟩
ISSAC
ISSAC 2020-45th International Symposium on Symbolic and Algebraic Computation
ISSAC 2020-45th International Symposium on Symbolic and Algebraic Computation, Jul 2020, Kalamata, Greece. pp.352-359, ⟨10.1145/3373207.3404029⟩
ISSAC 2020: 45th International Symposium on Symbolic and Algebraic Computation
ISSAC 2020: 45th International Symposium on Symbolic and Algebraic Computation, Jul 2020, Kalamata, Greece
Journal of Symbolic Computation
Journal of Symbolic Computation, 2023, 115, pp.74-95. ⟨10.1016/j.jsc.2022.07.007⟩
ISSAC
ISSAC 2020-45th International Symposium on Symbolic and Algebraic Computation
ISSAC 2020-45th International Symposium on Symbolic and Algebraic Computation, Jul 2020, Kalamata, Greece. pp.352-359, ⟨10.1145/3373207.3404029⟩
International audience; Arbitrary-precision integer libraries such as GMP are a critical building block of computer algebra systems. GMP provides state-of-the-art algorithms that are intricate enough to justify formal verification. In this paper, we
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5a3fc5c5c46d79e0759c236e8f996f20
https://hal.inria.fr/hal-02566654/file/main.pdf
https://hal.inria.fr/hal-02566654/file/main.pdf
Publikováno v:
ARITH-26 2019-26th IEEE 26th Symposium on Computer Arithmetic
ARITH-26 2019-26th IEEE 26th Symposium on Computer Arithmetic, Jun 2019, Kyoto, Japan. pp.183-186, ⟨10.1109/ARITH.2019.00041⟩
ARITH
ARITH-26 2019-26th IEEE 26th Symposium on Computer Arithmetic, Jun 2019, Kyoto, Japan. pp.183-186, ⟨10.1109/ARITH.2019.00041⟩
ARITH
International audience; We present the automatic formal verification of a state-of-the-art algorithm from the GMP library that computes the square root of a 64-bit integer. Although it uses only integer operations, the best way to understand the prog
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d142b5083514e669f442b7ac043cf3ae
https://inria.hal.science/hal-02092970/file/main.pdf
https://inria.hal.science/hal-02092970/file/main.pdf
Publikováno v:
Automated Reasoning ISBN: 9783319942049
IJCAR
9th International Joint Conference on Automated Reasoning
9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.178-193, ⟨10.1007/978-3-319-94205-6_13⟩
IJCAR
9th International Joint Conference on Automated Reasoning
9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.178-193, ⟨10.1007/978-3-319-94205-6_13⟩
International audience; Earlier work showed that automatic verification of GMP's algorithms using Why3 exceeds the current capabilities of automatic solvers. To complete this verification, numerous cut indications had to be supplied by the user, slow
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f0a6a39ffd02e658c01282a7f3fdbddb
https://doi.org/10.1007/978-3-319-94205-6_13
https://doi.org/10.1007/978-3-319-94205-6_13
Publikováno v:
9th Working Conference on Verified Software: Theories, Tools, and Experiments
9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. pp.84-101, ⟨10.1007/978-3-319-72308-2_6⟩
Lecture Notes in Computer Science ISBN: 9783319723075
VSTTE
9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. pp.84-101, ⟨10.1007/978-3-319-72308-2_6⟩
Lecture Notes in Computer Science ISBN: 9783319723075
VSTTE
International audience; The GNU Multi-Precision library is a widely used, safety-critical, library for arbitrary-precision arithmetic. Its source code is written in C and assembly, and includes intricate state-of-the-art algorithms for the sake of hi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::37e47fedf3db98f5cd6326fd62d26044
https://hal.inria.fr/hal-01519732
https://hal.inria.fr/hal-01519732
Autor:
Raphael Rieu-Helft
Publikováno v:
Journal of Formalized Reasoning, Vol 12, Iss 1, Pp 53-97 (2019)
Large-integer arithmetic algorithms are used in contexts where both their performance and their correctness are critical, such as cryptographic software. The fastest algorithms are complex enough that formally verifying them is desirable but challeng
Externí odkaz:
https://doaj.org/article/28ffe5e95b5d4663a408aa4d352c1eb1
