Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem

被引：0
作者：
Soares, Tiago Lopes [1 ]
Chirica, Ion [1 ]
Pereira, Mario [1 ]
机构：
[1] Nova Sch Sci & Technol, NOVA LINCS, Lisbon, Portugal
来源：
LEVERAGING APPLICATIONS OF FORMAL METHOD, VERIFICATION AND VALIDATION: SPECIFICATION AND VERIFICATION, PT III, ISOLA 2024 | 2025年 / 15221卷
关键词：
Software Verification; Dynamic Analysis; Deductive Software Verification; Gospel; OCaml; Ortac; Cameleer; CFML; RUNTIME ASSERTION CHECKING; TOOL;
D O I：
10.1007/978-3-031-75380-0_14
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We present our work on the collaborative use of dynamic and static analysis tools for the verification of software written in the OCaml language. We build upon Gospel, a specification language for OCaml that can be used both in dynamic and static analyses. We employ Ortac, for runtime assertion checking, and Cameleer and CFML for the deductive verification of OCaml code. We report on the use of such tools to build a case study of collaborative analysis of a non-trivial OCaml program. This shows how these tools nicely complement each others, while at the same highlights the differences when writing specification targeting dynamic or static analysis methods.
引用
收藏
页码：247 / 265
页数：19
相关论文
共 35 条
  • [1] [Anonymous], 2011, Lecture Notes in Computer Science, DOI [DOI 10.1007/978-3-642-35746-6_3, DOI 10.1007/978-3-642-35746-63]
  • [2] Baudin P., 2024, ACSL: ANSI/ISO C Specification Language
  • [3] Bobot F., 2012, BOOG 2011 1 INT WORK
  • [4] Carre B., 1990, Proceedings TRI-Ada '90, P392, DOI 10.1145/255471.255563
  • [5] Separation Logic for Sequential Programs (Functional Pearl)
    Chargueraud, Arthur
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (ICFP):
  • [6] Charguéraud A, 2019, LECT NOTES COMPUT SC, V11800, P484, DOI 10.1007/978-3-030-30942-8_29
  • [7] Characteristic Formulae for the Verification of Imperative Programs
    Chargueraud, Arthur
    [J]. ACM SIGPLAN NOTICES, 2011, 46 (09) : 418 - 430
  • [8] QuickCheck: A lightweight tool for random testing of Haskell programs
    Claessen, K
    Hughes, J
    [J]. ACM SIGPLAN NOTICES, 2000, 35 (09) : 268 - 279
  • [9] Clarke L. A., 2006, Software Engineering Notes, V31, P25, DOI 10.1145/1127878.1127900
  • [10] JML and OpenJML for Java']Java 16
    Cok, David R.
    [J]. PROCEEDINGS OF THE 23RD ACM INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS (FTFJP '21), 2021, : 65 - 67
1234