Voltar
Capítulo de livro Acesso aberto Revisado por pares
BIBTEX RIS

Cameleer: A Deductive Verification Tool for OCaml

2021; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-030-81688-9_31

ISSN

1611-3349

Autores

Mário Pereira, António Ravara,

Tópico(s)

Software Engineering Research

Resumo

Abstract We present , an automated deductive verification tool for OCaml. We leverage on the recently proposed GOSPEL (Generic OCaml SPEcification Language) to attach rigorous, yet readable, behavioral specification to OCaml code. The formally-specified program is fed to our toolchain, which translates it into an equivalent one in WhyML, the programming and specification language of the Why3 verification framework. We report on successful case studies conducted in .

Referência(s)