RSS Meetup

Cameleer: a Deductive Verification Tool for OCaml

Transmissão através de Videoconferência
Logótipo do LASIGE

Por Mário Pereira (NOVA-LINCS, FCT/UNL).

OCaml is particularly well-fitted for formal verification. On one hand, it is a multiparadigm 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. Cameleer is a Horizon 2020 project (Grant agreement ID: 897873) under the Marie Skłodowska-Curie individual fellowships action.

Zoom link: https://videoconf-colibri.zoom.us/j/89091398408.

Cameleer: a Deductive Verification Tool for OCaml

15h00
LASIGE

Solid Earth Seminar, por Débora Duarte (Royal Holloway - University of London, UK).

Seminário de Pós-graduação (Doutoramento em Biologia), por Liliana Andreia dos Santos Ferreira.

Fotografia de cigarra e informações relacionadas com o concurso

Onde vivem as 13 espécies de cigarras conhecidas em Portugal? É este o desafio lançado pelo projeto Cigarras de Portugal, do cE3c.

Representação da cidade de Lisboa, acompanhada do título da conferência

The scientific programme addresses a broad range of topics at the interface between particle, nuclear and astrophysics. Special emphasis will be devoted to recent discoveries and results.

The International Doctorate Network in Particle Physics, Astrophysics and Cosmology (IDPASC) is an interdisciplinary network whose aim is to train a new generation of high-level experts in the fields of Particle Physics, Astrophysics and Cosmology.

Título do evento, acompanhado dos logótipos do Tec Labs e de Ciências ULisboa

Applications until 12 August 2021.

Logótipo da Unite!

Summer School no âmbito da Rede UNITE! (University Network for Innovation, Technology and Engineering), de que faz parte a ULisboa.

O curso visa apresentar uma série de perspetivas sobre o desenvolvimento conceitual da estatística e sobre o uso de inferências e modelos estatísticos nas ciências empíricas.

Imagem ilustrativa do curso, acompanhada de várias informações úteis

Um curso dirigido ao público em geral e a estudantes de arte ou ciência (a partir dos 16 anos), com interesse em desenho de observação, ilustração e biologia, com ou sem experiência em desenho.

The objective of this course is to introduce participants to the details of communication and writing scientific publications.

The objective of this course is to introduce participants to the details of communicating science to non-specialized audiences, including, but not exclusive to, public and private stakeholders, students and teachers, and media professionals.

This course aims to evidence the importance of natural history collections for the study of biodiversity, to show new tools and approaches to extract and disseminate biodiversity data from natural history collections and to increase awareness of young researchers for the scientific and cultural value of Natural History Museums.

The course aims at providing an introduction to stable isotopes ratios as tools to understand global, ecosystem and community level bio/geo cycles; light isotopes: H, N, C, O and S isotopes, geo cycles and ecological significance; sampling and analytical methodologies in stable isotope analysis.

EvoS aims at turning evolutionary theory into a common language to areas that pertain to the natural world, including human affairs.

The course SoilEco aims at introducing attendants to an updated state of the art of diversity of the soil biota and the functional roles played by soil organisms in key ecological processes.

In this course, we promote a multidisciplinary approach presenting the most recent findings on the topic and challenging the traditional way of considering symbiotic associations as exceptions and not as the rule.

The goal of this course is to provide to the participants with current and practical knowledge on urban ecology, including ecological and social aspects.

This course aims to explore ways of communicating science to non-specialized audiences, such as policy makers, industry, general public (including students and teachers), through their engagement and participation in citizen science activities.