WhyMP, a Formally Verified Arbitrary-Precision Integer Library
| Autor: | Guillaume Melquiond, Raphaël Rieu-Helft |
|---|---|
| Přispěvatelé: | Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), TrustInSoft (TIS ), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Correctness
Algebra and Number Theory Interface (Java) Programming language [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic Mathematical library [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 02 engineering and technology Integer arithmetic Symbolic computation computer.software_genre 020202 computer hardware & architecture Automated theorem proving Computational Mathematics Arbitrary-precision arithmetic ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION 0202 electrical engineering electronic engineering information engineering Deductive program verification 020201 artificial intelligence & image processing Formal verification computer Block (data storage) Integer (computer science) Mathematics |
| Zdroj: | 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⟩ |
| ISSN: | 0747-7171 1095-855X |
| DOI: | 10.1016/j.jsc.2022.07.007⟩ |
| Popis: | 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 present a C library that has been formally verified using the Why3 verification platform in about four person-years. This verification deals not only with safety, but with full functional correctness. It has been performed using a mixture of mechanically checked handwritten proofs and automated theorem proving. We have implemented and verified a nontrivial subset of GMP's algorithms, including their optimizations and intricacies. Our library provides the same interface as GMP and is almost as efficient for smaller inputs. We detail our verification methodology and the algorithms we have implemented, and include some benchmarks to compare our library with GMP. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect