publication . Preprint . 2018

A Toolchain to Produce Correct-by-Construction OCaml Programs

Filliâtre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei; Pereira, Mário; Melo De Sousa, Simão;
Open Access English
  • Published: 02 May 2018
  • Publisher: HAL CCSD
Abstract
This paper presents a methodology to get correct-by-construction OCaml programs using the Why3 tool. First, a formal behavioral specification is given in the form of an OCaml module signature extended with type invariants and function contracts, in the spirit of JML. Second, an implementation is written in the programming language of Why3 and then verified with respect to the specification. Finally, an OCaml program is obtained by an automated translation. Our methodology is illustrated with the proof of a union-find library. Several other proofs of data structures and algorithms are included in the companion artifact to this paper.
Subjects
ACM Computing Classification System: TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Download from

1. Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.4, 2009. http://frama-c.cea.fr/acsl.html.

2. Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joeseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT), 7(3):212-232, June 2005.

3. Rod Burstall. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, 7:23-50, 1972.

4. Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (ICFP), pages 418-430, Tokyo, Japan, September 2011. ACM.

5. Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, and François Pottier. VOCAL - A Verified OCaml Library. ML Family Workshop, September 2017. [OpenAIRE]

6. Arthur Charguéraud and François Pottier. Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Journal of Automated Reasoning, September 2017.

7. Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. A pragmatic type system for deductive verification. Research report, Université Paris Sud, 2016. https://hal.archives-ouvertes.fr/hal-01256434v3.

8. Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 247-259, Mumbai, India, January 2015. ACM.

9. Jason Koenig and K. Rustan M. Leino. Programming language features for refinement. In John Derrick, Eerke A. Boiten, and Steve Reeves, editors, Proceedings 17th International Workshop on Refinement, Refine@FM 2015, Oslo, Norway, 22nd June 2015., volume 209 of EPTCS, pages 87-106, 2015.

10. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In LPAR-16, volume 6355 of Lecture Notes in Computer Science, pages 348-370. Springer, 2010. [OpenAIRE]

11. Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363-446, 2009. [OpenAIRE]

12. Pierre Letouzey. A new extraction for Coq. In Herman Geuvers and Freek Wiedijk, editors, TYPES 2002, volume 2646 of Lecture Notes in Computer Science. Springer, 2003. [OpenAIRE]

13. François Pottier. Verifying a hash table and its iterators in higher-order separation logic. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), January 2017.

Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue