Prototype

Inscrições em Minicurso -> PVS : Uma Introdução

Minicurso: PVS: Uma Introdução
 
Ministrante: Andréia Borges Avelar

Resumo: 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.

Data:  16, 17 e 18 de abril

Horário: 16/04: 10:00hs
               17/04: 8:30hs
               18/04: 10:00 hs

Local:   Laboratório de Informática do IME.

Inscrições: As inscrições devem ser realizadas em:

Número de vagas: 16

Bio: Andréia Avelar possui graduação em Bacharelado em Matemática pela Universidade de Brasília (2005), mestrado em Matemática pela Universidade de Brasília (2009) e doutorado em Matemática pela Universidade de Brasília (2014). Atualmente é professora na categoria "Adjunto 1" da Universidade de Brasília. Tem experiência na área de Matemática, com ênfase em Teoria da Computação. Parte do seu doutorado foi realizado no National Institute of Aerospace (NIA) vinculado a NASA, sob supervisão do pesquisador do NASA LaRC César A. Muñoz. Desenvolveu a biblioteca CCG e contribuiu com as bibliotecas TRS e digraphs presentes na nasalib (biblioteca oficial de formalizações em PVS da NASA).