Formalização de Teoremas em Assistentes de Prova

XXIX Semana do IME/UFG e VI Seminário de Pesquisa e Pós-Graduação do IME/UFG , Goiânia
Aulas: 06 de Outubro(Quarta-feira) a 08 de Outubro (Sexta-feira)

Informações gerais

Utilizaremos o assistente de provas PVS(versão 7.1), no ambiente integrado para PVS dentro do software VS-Code (VSCode-PVS IDE).
Não é mandatória a instalação do PVS para acompanhar o curso, contudo encorajamos que os participantes façam a instalação do
sistema em suas máquinas para, fora da aula, trabalharem nos exercícios que serão disponibilizados.

• É possível instalar o VSCode-PVS diretamente do Marketplace do VSCode.
• Utilizaremos as bibliotecas de PVS da NASA (NASALib) em alguns exemplos e exercícios.
• O PVS, nativamente, é executado sobre plataformas Unix ou MacOS (exceto, por enquanto, em arquiteturas M1).
  Para plataforma Windows ou MacOS com chip M1 é necessário instalar uma máquina virtual.

Programa e Material

• Aula 1 : 08:00 - 09:30 - 06 de Outubro, 2021
• Aula 2 : 08:00 - 09:30 - 07 de Outubro, 2021
• Aula 3 : 08:00 - 09:30 - 08 de Outubro, 2021

Palestrantes

• Mauricio Ayala-Rincón(UnB)
• Thaynara Arielly de Lima (UFG)