A carregar...
Publicação
Practical Deductive Verification of OCaml Programs
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 1.87 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
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.
Descrição
Publisher Copyright: © The Author(s) 2025.
Palavras-chave
Cameleer Deductive Software Verification GOSPEL OCaml Theoretical Computer Science General Computer Science
Contexto Educativo
Citação
Editora
Springer Science and Business Media Deutschland GmbH