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 条
  • [41] Region analysis for deductive verification of C programs
    M. U. Mandrykin
    A. V. Khoroshilov
    Programming and Computer Software, 2016, 42 : 257 - 278
  • [42] Incremental Deductive Verification for Relational Model Transformations
    Cheng, Zheng
    Tisi, Massimo
    2017 10TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST), 2017, : 379 - 389
  • [43] Deductive verification of solidity smart contracts with SSCalc
    Marmsoler, Diego
    Thornton, Billy
    SCIENCE OF COMPUTER PROGRAMMING, 2025, 243
  • [44] RHLE: Modular Deductive Verification of Relational ∀∃ Properties
    Dickerson, Robert
    Ye, Qianchuan
    Zhang, Michael K.
    Delaware, Benjamin
    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2022, 2022, 13658 : 67 - 87
  • [45] Deductive verification of simple foraging robotic behaviours
    Behdenna, Abdelkader
    Dixon, Clare
    Fisher, Michael
    INTERNATIONAL JOURNAL OF INTELLIGENT COMPUTING AND CYBERNETICS, 2009, 2 (04) : 604 - 643
  • [46] Deductive verification of invariants of state-transition systems
    Hutter, D
    KI-98: ADVANCES IN ARTIFICIAL INTELLIGENCE, 1998, 1504 : 153 - 164
  • [47] Modular Deductive Verification of Sampled-Data Systems
    Ricketts, Daniel
    Malecha, Gregory
    Lerner, Sorin
    2016 PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE (EMSOFT), 2016,
  • [48] Deductive verification of probabilistic real-time systems
    Yamane, S
    24TH INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS WORKSHOPS, PROCEEDINGS, 2004, : 622 - 627
  • [49] Modularity for Decidability of Deductive Verification with Applications to Distributed Systems
    Taube, Marcelo
    Losa, Giuliano
    McMillan, Kenneth L.
    Padon, Oded
    Sagiv, Mooly
    Shoham, Sharon
    Wilcox, James R.
    Woos, Doug
    ACM SIGPLAN NOTICES, 2018, 53 (04) : 662 - 677
  • [50] Deductive Verification of Parameterized Embedded Systems Modeled in SystemC
    Tasche, Philip
    Monti, Raul E.
    Drerup, Stefanie Eva
    Blohm, Pauline
    Herber, Paula
    Huisman, Marieke
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2024, PT II, 2024, 14500 : 187 - 209
12345