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 条
  • [21] Automated Deductive Verification for Ladder Programming
    Cousineau, Denis
    Mentre, David
    Inoue, Hiroaki
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2019, (310): : 7 - 12
  • [22] Deductive Verification in Decidable Fragments with Ivy
    McMillan, Kenneth L.
    Padon, Oded
    STATIC ANALYSIS (SAS 2018), 2018, 11002 : 43 - 55
  • [23] Algorithmic and deductive verification methods for CTL
    Pnueli, A
    Kesten, Y
    MODELS, ALGEBRAS AND LOGIC OF ENGINEERING SOFTWARE, 2003, 191 : 109 - 131
  • [24] Deductive verification of active objects with Crowbar
    Kamburjan, Eduard
    Scaletta, Marco
    Rollshausen, Nils
    SCIENCE OF COMPUTER PROGRAMMING, 2023, 226
  • [25] Deductive verification of the sliding window protocol
    Chkliaev D.A.
    Nepomniaschy V.A.
    Automatic Control and Computer Sciences, 1600, Allerton Press Incorporation (47): : 420 - 426
  • [26] Deductive verification of UML models in TLPVS
    Arons, T
    Hooman, J
    Kugler, H
    Pnueli, A
    van der Zwaag, M
    UML 2004 - THE UNIFIED MODELING LANGUAGE: MODELING LANGUAGES AND APPLICATIONS, PROCEEDINGS, 2004, 3273 : 335 - 349
  • [27] Deductive verification of smart contracts with Dafny
    Cassez, Franck
    Fuller, Joanne
    Quiles, Horacio Mijail Anton
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2024, 26 (02) : 131 - 145
  • [28] Kmclib: Automated Inference and Verification of Session Types from OCaml Programs
    Imai, Keigo
    Lange, Julien
    Neykova, Rumyana
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I, 2022, 13243 : 379 - 386
  • [29] ROTOR: A Tool for Renaming Values in OCaml's Module System
    Rowe, Reuben N. S.
    Feree, Hugo
    Thompson, Simon J.
    Owens, Scott
    2019 IEEE/ACM 3RD INTERNATIONAL WORKSHOP ON REFACTORING (IWOR 2019), 2019, : 27 - 30
  • [30] Simulation and verification of protocol using deductive machine
    Lai, R
    Li, X
    SIMULATION, 1995, 65 (05) : 321 - 333
12345