O PVS (Prototype Verification System) é um sistema de especificação e verificação formal, desenvolvido por SRI International, que provê um ambiente integrado para desenvolvimento e análise de especificações formais, com suporte a uma ampla gama de atividades envolvendo criação, análise, modificação, gerenciamento e documentação de teorias e provas. O PVS é uma ferramenta fundamental em vários projetos envolvendo verificação formal desenvolvidos pelo grupo de métodos formais do NASA Langley Research Center (NASA LaRC), por essa razão existe um esforço contínuo dos pesquisadores do NASA LaRC no sentido de desenvolver técnicas de verificação formal integradas ao PVS visando uma variedade de aplicações, originando assim uma grande coleção de teorias envolvendo verificações formais importantes que vão desde teorias matemáticas complexas em álgebra, análise e teoria de conjuntos por exemplo, até especificações e formalizações de modelos para a verificação de sistemas de tráfego aéreo e de protocolos de tolerância a falhas.

O objetivo desse curso é oferecer uma introdução ao sistema, apresentando os aspectos básicos da linguagem de especificação e do provador, propiciando assim ao usuário iniciante no sistema as ferramentas e habilidades necessárias para especificar teorias e formalizar teoremas utilizando o PVS.

Informações

• Data: 16, 17 e 18 de abril
• Horário: 16 às 10:00hs; 17 às 8:30hs e 18 às 10:00hs
• Local: Laboratório de Informática do IME-UFG