GOSPEL - Providing OCaml with a Formal Specification Language
This work introduces GOSPEL, a behavioral specification language for OCaml. It is designed to enable modular verification of data structures and algorithms. GOSPEL is a contract-based, strongly typed language, with a formal semantics defined by means of translation into Separation Logic. Compared with writing specifications directly in Separation Logic, GOSPEL provides a high-level syntax that greatly improves conciseness and makes it accessible to programmers with no familiarity with Separation Logic. Although GOSPEL has been developed for specifying OCaml code, we believe that many aspects of its design could apply to other programming languages. This work presents the design and semantics of GOSPEL, and reports on its application for the development of a formally verified library of general-purpose OCaml data structures. This is joint work with Arthur Charguéraud, Jean-Christophe Filliâtre and Cláudio Lourenço, and was presented at the 23rd International Symposium on Formal Methods, part of the 3rd World Congress on Formal Methods.
16/10/2019 13:00
Software Systems
Mário is a postdoctoral researcher, associated with NOVA LINCS. He got his PhD from Université Paris-Saclay, France, in 2018, where we was affiliated with LRI (Laboratoire de Recherche en Informatique), France, working within the Why3 team, under the supervision of Jean-Christophe Filliâtre. Mário got his BSc engineering degree from Universidade da Beira Interior (ranked 1st) and MSc degree (major in logic and computation) from FCUP, Porto (ranked 1st). Mário's research interests are mainly deductive software verification, functional programming, type systems, module systems, and program transformations. Mário is the winner of the software competition VerifyThis in 2016 and 2017 editions. Mário is a developer of the Why3 verification platform, as well as of the VOCAL library, the mechanically verified OCaml library.
