Publicação
Practical Deductive Verification of OCaml Programs
| dc.contributor.author | Pereira, Mário | |
| dc.contributor.institution | NOVALincs | |
| dc.date.accessioned | 2025-07-07T21:19:13Z | |
| dc.date.available | 2025-07-07T21:19:13Z | |
| dc.date.issued | 2025 | |
| dc.description | Publisher Copyright: © The Author(s) 2025. | |
| dc.description.abstract | 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. | en |
| dc.description.version | publishersversion | |
| dc.description.version | published | |
| dc.format.extent | 25 | |
| dc.format.extent | 1962406 | |
| dc.identifier.doi | 10.1007/978-3-031-71177-0_29 | |
| dc.identifier.isbn | 9783031711763 | |
| dc.identifier.issn | 0302-9743 | |
| dc.identifier.other | PURE: 112634730 | |
| dc.identifier.other | PURE UUID: cc5fcf1b-a28a-44a4-9f6b-4956f620ad2f | |
| dc.identifier.other | Scopus: 85205133549 | |
| dc.identifier.other | ORCID: /0000-0003-4234-5376/work/187481873 | |
| dc.identifier.uri | http://hdl.handle.net/10362/184925 | |
| dc.identifier.url | https://www.scopus.com/pages/publications/85205133549 | |
| dc.language.iso | eng | |
| dc.peerreviewed | yes | |
| dc.publisher | Springer Science and Business Media Deutschland GmbH | |
| dc.subject | Cameleer | |
| dc.subject | Deductive Software Verification | |
| dc.subject | GOSPEL | |
| dc.subject | OCaml | |
| dc.subject | Theoretical Computer Science | |
| dc.subject | General Computer Science | |
| dc.title | Practical Deductive Verification of OCaml Programs | en |
| dc.type | conference object | |
| degois.publication.firstPage | 518 | |
| degois.publication.lastPage | 542 | |
| degois.publication.title | Formal Methods - 26th International Symposium, FM 2024, Proceedings Part II | |
| degois.publication.title | 26th International Symposium on Formal Methods, FM 2024 | |
| dspace.entity.type | Publication | |
| rcaap.rights | openAccess |
Ficheiros
Principais
1 - 1 de 1
A carregar...
- Nome:
- Practical_Deductive_Verification_of_OCaml_Programs.pdf
- Tamanho:
- 1.87 MB
- Formato:
- Adobe Portable Document Format