No próximo dia 22 de julho de 2021, pelas 14h, Mário Pereira irá dar uma palestra intitulada "Cameleer: s Deductuve Verification Tool for OCaml".
A palestra é organizada pelo DCC-FCUP e pelo grupo de investigação HASLab - INESCTEC e é aberta a todos os interessados.
A sessão será de forma remota. A participação é gratuita, mas a inscrição é obrigatória.
Short Bio
Mário Pereira is a Marie Skłodowska-Curie fellow, 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 is also the winner of the software competition VerifyThis in 2016 and 2017 editions. His main research interests are software verification and functional programming, on the large. He is the leading architect and developer of the Cameleer tool, a deductive verification tool for OCaml-written code, with a clear focus on proof automation. Mário is also a developer of the Why3 framework, as well as of the VOCAL library, the mechanically verified OCaml library, and the GOSPEL specification language.
Title
Cameleer: a Deductive Verification Tool for OCaml
Abstract
OCaml is particularly well-fitted for formal verification. On one hand, it is a multi-paradigm language with well-defined semantics, allowing one to write clean, concise, type-safe, and efficient code. On the other hand, it is a language of choice for the implementation of sensible software, e.g., industrial compilers, proof assistants, and automated solvers. Yet, with the notable exception of some interactive tools, formal verification has been seldom applied to OCaml-written programs. In this talk, we present the ongoing project Cameleer, aiming for the development of a deductive verification tool for OCaml, with a clear focus on proof automation. 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 program in WhyML, the programming and specification language of the Why3 verification framework. Finally, Why3 is used to compute verification conditions for the generated program, which can be discharged by off-the-shelf SMT solvers. We present successful applications of the Cameleer tool to prove functional correctness of several significant case studies, like FIFO queues (ephemeral and applicative implementations) and leftist heaps, issued from existing OCaml libraries. This is joint work with António Ravara, also associated with NOVA LINCS. Cameleer is a Horizon 2020 project (Grant agreement ID: 897873) under the Marie Skłodowska-Curie individual fellowships action.