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

The objective of this course is to introduce participants to the details of communication and writing scientific publications. The main emphasis is on the most common form, the “primary scientific paper”, but other forms will be covered.

O curso pretende fornecer as ferramentas necessárias para que o investigador na área da saúde consiga desenvolver autonomia para o desenvolvimento de trabalhos de investigação científica utilizando a metodologia estatística apropriada.

Mathematical Logic Webinar, por Bruno Jacinto (Universidade de Lisboa) e José Mestre (Stirling (SASP) e LanCog (Lisboa)).

Logótipo da Rede Campus Sustentável

Serão abordados conceitos e aplicações da economia circular em algumas cadeias de valor dos produtos, evidenciando um exemplo de boas práticas como o caso do projeto Permalab de Ciências ULisboa com a apresentação de soluções de permacultura urbana.

Através de 4 módulos e com recurso ao software R, aprenda a organizar e analisar dados com foco na obtenção de soluções orientadas para a resolução de problemas.

Imagem ilustrativa do evento, acompanhada das datas de realização e de outras informações relevantes

Um curso dedicado a todos aqueles que se interessam pelo conhecimento.

Fotografia de palestra a decorrer nas instalações de Ciências ULisboa

Encontro de Comunicação de Ciência(s), por Amelia Ortiz-Gil (Universidad de Valencia), Francesca Primas (European Southern Observatory) e Jake Noel-Storr (University of Groningen).

Sessão da Classe de Ciências da Academia das Ciências de Lisboa, por Maria Ivette Gomes (Ciências ULisboa).

Geometry Webinar, por André Oliveira (CMUP).

This course is conceived to give an integrated view of the living component of soils, and its key role on ecosystem functions and processes.

Seminário Permanente de Filosofia das Ciências, por José Ferreirós (Universidade de Sevilha).

Sessão de esclarecimento e divulgação da Bolsa Fulbright para Investigação com o apoio da FCT.

Título da iniciativa, sobre uma imagem estilizada de Lisboa (Praça do Comércio)

Candidaturas a decorrer até 30 de janeiro de 2021.

Imagem ilustrativa do evento, acompanhada da data de realização

Evento final do projeto europeu PROSEU - PROSumers of the Energy Union: mainstreaming active participation of citizens in the energy transition.

Fotografia de pessoas, acompanhada do título da iniciativa

A ULisboa promove o Dia Aberto M23, um evento que pretende aproximar o público adulto do meio universitário.

Imagem ilustrativa do concurso, acompanhada do respetivo logótipo

Candidaturas para a 2.ª edição do Campus 2030 a decorrer até 07 de fevereiro de 2021 - uma oportunidade para estudantes, professores e investigadores converterem o seu campus num modelo global de sustentabilidade.

This course promotes 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.

Imagem ilustrativa da iniciativa (ameaças à vida marinha)

O projeto visa apresentar soluções que contribuam para o desafio atual da sustentabilidade dos Oceanos - candidaturas até 15 de fevereiro de 2021.

Feixes luminosos

Ação de formação dirigida aos docentes e investigadores de Ciências ULisboa, pela formadora Sofia Sá.

Geometry Webinar, por Thomas Krämer (Humboldt Universität zu Berlin).

A disseminação da SARS-CoV 2 faz centrar na vacinação a melhor expectativa para suster a pandemia, e retoma a reflexão sobre os valores que a sua administração põe em confronto.

Imagem ilustrativa do prémio

Um prémio dirigido aos jovens investigadores a trabalhar em Portugal com objetivos de investigação centrados no Atlântico, com candidaturas entre 01 e 28 de fevereiro de 2021.

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

This course aims at exploring how scientists can use social media as tools to enhance the communication of their research and the dialogue with society, and discussing the differences that exist in the work of scientists and journalists in terms of the methods and deadlines they meet and exploring how scientists and journalists can better articulate.

Páginas