Apresentações VFS

11/07/2012-- Anfiteatro 2
  • 9h:00 : Verificação de programas em C por abstracção de predicados. João Graça
  • 9h: 25: Model Checking para sistemas temporizados: autómatos temporizados. Hugo Sousa
  • 9h:50: Anotações e extensões da lógica de Hoare para linguagens orientadas a objectos. José Carvalho
  • 10h 15: Verificação de programas orientados a objectos usando o KeY. Gonçalo Martins
  • Intervalo
  • 11h 00: Lógicas para sistemas Hibrídos - Keymaera. André Gaspar
  • 11h25: Teorias decidíveis para resolutores SAT-DPPL: arrays e lógica de apontadores. Susana João
  • 11h50:Teorias decidíveis para resolutores SAT-DPPL: vectores de bits. Maria Nelson
  • 12h15: Model Checker SPIN e linguagem de especificação Promela. Armindo Cunha
  • Almoço
  • 14h30: SLAM2. João Viana
  • 14h55: Palavras imbricadas e linguagens de autómatos de pilha com visibilidade.Francisco Mota
  • 15h20: WHY3:Linguagem Why3ML. Nuno Peralta
  • 15h55: Boogie:Linguagem intermédia e ferramente de verificação para .NET (Spec #) Armindo Pereira
  • Intervalo
  • 16h30:VCC: um verificador para C concurrente. João Proença
  • • 16h55: Alloy: Modelação Relacional de Sistemas. Tiago Melo