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.