Cameleer: A Deductive Verification Tool for OCaml

被引：5
|
作者：
Pereira, Mario [1 ]
Ravara, Antonio [1 ]
机构：
[1] Nova Sch Sci & Technol, NOVA LINCS, Lisbon, Portugal
来源：
COMPUTER AIDED VERIFICATION, PT II, CAV 2021 | 2021年 / 12760卷
关键词：
Deductive software verification; OCaml; Why3; GOSPEL;
D O I：
10.1007/978-3-030-81688-9_31
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
We present Cameleer, 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 Cameleer.
引用
收藏
页码：677 / 689
页数：13
相关论文
共 50 条
  • [1] Practical Deductive Verification of OCaml Programs
    Pereira, Mario
    FORMAL METHODS, PT II, FM 2024, 2025, 14934 : 518 - 542
  • [2] The Why//Krakatoa/Caduceus platform for deductive program verification -: (Tool paper)
    Filliatre, Jean-Christophe
    Marche, Claude
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2007, 4590 : 173 - +
  • [3] Deductive software verification
    Filliâtre J.-C.
    International Journal on Software Tools for Technology Transfer, 2011, 13 (5) : 397 - 403
  • [4] BSP-Why: A Tool for Deductive Verification of BSP Algorithms with Subgroup Synchronisation
    Jean Fortin
    Frédéric Gava
    International Journal of Parallel Programming, 2016, 44 : 574 - 597
  • [5] KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS
    Din, Crystal Chang
    Bubel, Richard
    Haehnle, Reiner
    AUTOMATED DEDUCTION - CADE-25, 2015, 9195 : 517 - 526
  • [6] BSP-Why: A Tool for Deductive Verification of BSP Algorithms with Subgroup Synchronisation
    Fortin, Jean
    Gava, Frederic
    INTERNATIONAL JOURNAL OF PARALLEL PROGRAMMING, 2016, 44 (03) : 574 - 597
  • [7] Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem
    Soares, Tiago Lopes
    Chirica, Ion
    Pereira, Mario
    LEVERAGING APPLICATIONS OF FORMAL METHOD, VERIFICATION AND VALIDATION: SPECIFICATION AND VERIFICATION, PT III, ISOLA 2024, 2025, 15221 : 247 - 265
  • [8] Deductive verification of modular systems
    Finkbeiner, B
    Manna, Z
    Sipma, HB
    COMPOSITIONALITY: THE SIGNIFICANT DIFFERENCE, 1998, 1536 : 239 - 275
  • [9] Deductive Verification of Legacy Code
    Beckert, Bernhard
    Bormer, Thorsten
    Grahl, Daniel
    LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I, 2016, 9952 : 749 - 765
  • [10] Deductive verification of cryptographic software
    Almeida, Jose Bacelar
    Barbosa, Manuel
    Pinto, Jorge Sousa
    Vieira, Barbara
    INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (03) : 203 - 218
12345