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 条
  • [31] Enhancing Automated Program Repair with Deductive Verification
    Le, Xuan-Bach D.
    Le, Quang Loc
    Lo, David
    Le Goues, Claire
    32ND IEEE INTERNATIONAL CONFERENCE ON SOFTWARE MAINTENANCE AND EVOLUTION (ICSME 2016), 2016, : 428 - 432
  • [32] Modular Deductive Verification of Multiprocessor Hardware Designs
    Vijayaraghavan, Muralidaran
    Chlipala, Adam
    Arvind
    Dave, Nirav
    COMPUTER AIDED VERIFICATION, CAV 2015, PT II, 2015, 9207 : 109 - 127
  • [33] A dynamic logic for deductive verification of concurrent programs
    Beckert, Bernhard
    Klebanov, Vladimir
    SEFM 2007: FIFTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2007, : 141 - +
  • [34] Deductive Verification of Chain-of-Thought Reasoning
    Ling, Zhan
    Fang, Yunhao
    Li, Xuanlin
    Huang, Zhiao
    Lee, Mingu
    Memisevic, Roland
    Su, Hao
    ADVANCES IN NEURAL INFORMATION PROCESSING SYSTEMS 36 (NEURIPS 2023), 2023,
  • [35] Region analysis for deductive verification of C programs
    Mandrykin, M. U.
    Khoroshilov, A. V.
    PROGRAMMING AND COMPUTER SOFTWARE, 2016, 42 (05) : 257 - 278
  • [36] Requirement Patterns in Deductive Verification of poST Programs
    Chernenko, I. M.
    Anureev, I. S.
    Garanina, N. O.
    AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2024, 58 (07) : 1003 - 1024
  • [37] Deductive verification of hybrid systems using STeP
    Manna, Z
    Sipma, HB
    HYBRID SYSTEMS: COMPUTATION AND CONTROL, 1998, 1386 : 305 - 318
  • [38] Deductive verification of telecommunication systems written in C
    Anureev I.S.
    Automatic Control and Computer Sciences, 2013, 47 (7) : 413 - 419
  • [39] Deductive Verification via the Debug Adapter Protocol
    Ernst, Gidon
    Blau, Johannes
    Murray, Toby
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (338): : 89 - 96
  • [40] A Sound and Complete Deductive System for CTL* Verification
    Gabbay, Dov M.
    Pnueli, Amir
    LOGIC JOURNAL OF THE IGPL, 2008, 16 (06) : 499 - 536
12345