TY - GEN
T1 - Practical Deductive Verification of OCaml Programs
AU - Pereira, Mário
N1 - Publisher Copyright:
© The Author(s) 2025.
PY - 2025
Y1 - 2025
N2 - 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.
AB - 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.
KW - Cameleer
KW - Deductive Software Verification
KW - GOSPEL
KW - OCaml
UR - https://www.scopus.com/pages/publications/85205133549
U2 - 10.1007/978-3-031-71177-0_29
DO - 10.1007/978-3-031-71177-0_29
M3 - Conference contribution
AN - SCOPUS:85205133549
SN - 9783031711763
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 518
EP - 542
BT - Formal Methods - 26th International Symposium, FM 2024, Proceedings Part II
A2 - Platzer, Andre
A2 - Rozier, Kristin Yvonne
A2 - Pradella, Matteo
A2 - Rossi, Matteo
PB - Springer Science and Business Media Deutschland GmbH
T2 - 26th International Symposium on Formal Methods, FM 2024
Y2 - 9 September 2024 through 13 September 2024
ER -