Name
Abstract | ||
|---|---|---|
We present a methodology, called OPEV, to validate the translation between OCaml and PVS, which supports non-executable semantics. This validation occurs by generating large-scale tests for OCaml implementations, generating test lemmas for PVS, and generating proofs that automatically discharge these lemmas. OPEV incorporates an intermediate type system that captures a large subset of OCaml types, employing a variety of rules to generate test cases for each type. To prove the PVS lemmas, we developed automatic proof strategies and discharged the test lemmas using PVS Proof-Lite, a powerful proof scripting utility of the PVS verification system. We demonstrated our approach on two case studies that include two hundred and fifty-nine functions selected from the Sail and Lem libraries. For each function, we generated thousands of test lemmas, all of which are automatically discharged. The methodology contributes to a reliable translation between OCaml and PVS. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/978-3-030-55754-6_12 | NFM |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Xiaoxin An | 1 | 0 | 0.34 |
| Amer Tahat | 2 | 0 | 0.34 |
| Binoy Ravindran | 3 | 0 | 0.34 |