Practical Deductive Verification of OCaml Programs (Extended Version)
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910536400109568 |
|---|---|
| author | Pereira, Mário |
| author_facet | Pereira, Mário |
| contents | In this paper, we provide a comprehensive, hands-on tutorial on how to apply deductive verification to programs written in OCaml. In particular, we show how one can use the GOSPEL specification language and the Cameleer tool to conduct mostly-automated verification on OCaml code. In our presentation, we focus on two main classes of programs: first, purely functional programs with no mutable state; then on imperative programs, where one can mix mutable state with subtle control-flow primitives, such as locally-defined exceptions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_17901 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Practical Deductive Verification of OCaml Programs (Extended Version) Pereira, Mário Logic in Computer Science In this paper, we provide a comprehensive, hands-on tutorial on how to apply deductive verification to programs written in OCaml. In particular, we show how one can use the GOSPEL specification language and the Cameleer tool to conduct mostly-automated verification on OCaml code. In our presentation, we focus on two main classes of programs: first, purely functional programs with no mutable state; then on imperative programs, where one can mix mutable state with subtle control-flow primitives, such as locally-defined exceptions. |
| title | Practical Deductive Verification of OCaml Programs (Extended Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2404.17901 |