Minds-on

Uma breve introdução à verificação de software

Num momento em que o software se tornou extremamente pervasivo, intervindo de forma totalmente autónoma, ou em direta interação com o utilizador num elevado número de aplicações das quais dependemos para realizar as tarefas do dia-a-dia, as falhas de software podem ter consequências catastróficas, incluindo em casos extremos, a perda de vidas humanas, dados irreparáveis no meio-ambiente, ou perdas avultadas de dinheiro. Tornou-se, por isso, evidente que é fundamental a utilização de ferramentas que permitam verificar, de forma inequívoca, se os requisitos de um sistema alvo se encontram corretamente implementados.

A abordagem tipicamente usada para identificar a potenciais erros de software passa pelo recurso a abordagens e ferramentas focadas na realização de testes (unitários, de integração, etc). Infelizmente, estas abordagens são extremamente custosas e incompletas no sentido de poderem falhar no objetivo de identificarem potenciais erros que apenas se revelam uma vez que o sistema em causa se encontre em operação.

Nesta sessão, será apresentada uma classe específica de demonstradores de teoremas automáticos “Satifiability Modulo Theories” (SMT), que combinam o conhecido problema da satisfazibilidade de programas Booleanos (SAT solvers) com teorias lógicas mais ricas e que permitem endereçar tarefas de verificação de código de programas. Iremos para tal utilizar a ferramenta Z3 da Microsoft Research que será, porventura, o demonstrador automático SMT mais evoluído e completo na atualidade, introduzir a audiência aos conceitos base que suportam este tipo de demonstrador automático e apresentar alguns exemplos simples codificados diretamente na ferramenta Z3 e através da utilização da API Python.

PRÉ-REQUISITOS (para atividades práticas):Não haverá lugar a atividades práticas.


  •  Oradores  
  •   Data e local
  •   Inscrições
  •  Informação Adicional

David Pereira

Data: 2021-06-02

Horário: 14h30

Duração: 1h

Local: Online via Microsoft Teams

As inscrições serão aceites por ordem de inscrição.

É necessário pré-inscrição a ser efectuada através de correio electrónico para a D. Lurdes Santos (MLSB@isep.ipp.pt)

Para mais informações: mindson@dei.isep.ipp.pt

Os workshops são gratuitos mas requerem inscrição, sendo o número de vagas limitado.