Embedding Untrusted Imperative ML Oracles into Coq Verified Code
In: https://hal.archives-ouvertes.fr/hal-02062288 ; 2019, 2019
Online
report
Zugriff:
This preprint has been largely rewritten and integrated into Sylvain Boulm{\'e}'s Habilitation in 2021, See http://www-verimag.imag.fr/~boulme/hdr.html. ; This paper investigates a lightweight approach-combining Coq and OCaml typecheckers-in order to formally verify higher-order imperative programs in partial correctness. In this approach, the user does never formally reason about effects of imperative functions, but only about their results. Formal guarantees are obtained by combining parametric reasoning over polymorphic functions (i.e. "theorems for free" a la Wadler) with verified defensive programming. This paper illustrates the approach on several examples. Among them: first, the certification of a polymorphic memoized fixpoint operator using untrusted hash-tables; second, a certified Boolean SAT-solver, invoking internally any untrusted but state-of-the-art SAT-solver (itself generally programmed in C/C++).
Titel: |
Embedding Untrusted Imperative ML Oracles into Coq Verified Code
|
---|---|
Autor/in / Beteiligte Person: | Boulmé, Sylvain ; Vandendorpe, Thomas ; VERIMAG (VERIMAG - IMAG) ; Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes 2016-2019 (UGA 2016-2019 ) |
Link: | |
Zeitschrift: | https://hal.archives-ouvertes.fr/hal-02062288 ; 2019, 2019 |
Veröffentlichung: | HAL CCSD, 2019 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|