تقرير
Practical Deductive Verification of OCaml Programs (Extended Version)
العنوان: | Practical Deductive Verification of OCaml Programs (Extended Version) |
---|---|
المؤلفون: | Pereira, Mário |
سنة النشر: | 2024 |
المجموعة: | Computer Science |
مصطلحات موضوعية: | Computer Science - Logic in Computer Science |
الوصف: | 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. |
نوع الوثيقة: | Working Paper |
URL الوصول: | http://arxiv.org/abs/2404.17901 |
رقم الأكسشن: | edsarx.2404.17901 |
قاعدة البيانات: | arXiv |
كن أول من يترك تعليقا!