A carregar...
Publicação
Practical deductive verification of OCaml programs
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 1.86 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
Despite all the tremendous recent advances in deductive software verification, this has seldom been applied to the verification of programs written in a functional language. In this paper, we give an overview of Cameleer , a verification tool that directly targets OCaml code and is built with a clear focus on proof automation. We leverage on Gospel (Generic OCaml SPEcification Language) to provide formal specification to OCaml implementations. We use a running example to illustrate the specification and verification process employed by Cameleer . Finally, we highlight the crucial impact of Cameleer in recent research and development projects.
Descrição
Publisher Copyright: © 2026 The Author(s).
Palavras-chave
Cameleer Deductive verification Gospel OCaml Why3 Software Information Systems Modelling and Simulation Computational Theory and Mathematics