Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911968382681088 |
|---|---|
| author | Soares, Tiago Lopes Chirica, Ion Pereira, Mário |
| author_facet | Soares, Tiago Lopes Chirica, Ion Pereira, Mário |
| contents | We present our work on the collaborative use of dynamic and static analysis tools for the verification of software written in the OCaml language. We build upon Gospel, a specification language for OCaml that can be used both in dynamic and static analyses. We employ Ortac, for runtime assertion checking, and Cameleer and CFML for the deductive verification of OCaml code. We report on the use of such tools to build a case study of collaborative analysis of a non-trivial OCaml program. This shows how these tools nicely complement each others, while at the same highlights the differences when writing specification targeting dynamic or static analysis methods. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_17289 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version) Soares, Tiago Lopes Chirica, Ion Pereira, Mário Logic in Computer Science We present our work on the collaborative use of dynamic and static analysis tools for the verification of software written in the OCaml language. We build upon Gospel, a specification language for OCaml that can be used both in dynamic and static analyses. We employ Ortac, for runtime assertion checking, and Cameleer and CFML for the deductive verification of OCaml code. We report on the use of such tools to build a case study of collaborative analysis of a non-trivial OCaml program. This shows how these tools nicely complement each others, while at the same highlights the differences when writing specification targeting dynamic or static analysis methods. |
| title | Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.17289 |