Palestra
11/6/2012, 14h30m DCC-FCUP Sala 2
Provas de programa em Why3 - uma introdução.
Orador: Simão Melo de Sousa, LIACC& UBI
Resumo:
Esta aula introduz pela prática a plataforma de verificação dedutiva de programas WHY3.
Começaremos por uma curta apresentação da linguagem de programação e da linguagem de especificação.
Em seguida mostramos como a lógica de Hoare simples é estendida para as construções programáticas why3.
Esta lógica e o seu cálculo de pre-condição mais fraca subjacente tornam esta ferramenta ideal para a prova de algoritmos, quaisquer que sejam estes, mas também de programas clássicos, desde que se consiga traduzir estes para a linguagem Why3ml.
Demonstraremos esta afirmação pela prática, mostrando como o why3 permite provar vários exemplos que introduziremos.
Realça-se em particular a prova de programas para a arquitectura ARM.
11/6/2012, 14h30m DCC-FCUP Sala 2
Provas de programa em Why3 - uma introdução.
Orador: Simão Melo de Sousa, LIACC& UBI
Resumo:
Esta aula introduz pela prática a plataforma de verificação dedutiva de programas WHY3.
Começaremos por uma curta apresentação da linguagem de programação e da linguagem de especificação.
Em seguida mostramos como a lógica de Hoare simples é estendida para as construções programáticas why3.
Esta lógica e o seu cálculo de pre-condição mais fraca subjacente tornam esta ferramenta ideal para a prova de algoritmos, quaisquer que sejam estes, mas também de programas clássicos, desde que se consiga traduzir estes para a linguagem Why3ml.
Demonstraremos esta afirmação pela prática, mostrando como o why3 permite provar vários exemplos que introduziremos.
Realça-se em particular a prova de programas para a arquitectura ARM.
Palestra
6/6/2012, 11h30m DCC-FCUP Sala 3.
Formal methods in industry: Educed's path to make it happen
Orador: José Miguel Faria, Leading founder
Resumo:
After a three months period of highly successful customer validation in Silicon Valley, interacting with world leader companies in the Aeronatics, Space and Medical Devices domains, Educed is back in Portugal fully focused on maturing its flagship product, PROVA.
PROVA offers companies a solution for drastically reducing the effort and cost of delivering top quality high-integrity software. It provides mathematically powerfull techniques for analysing and validating the textual requirements of a system, identifying possible ambiguities, omissions, and inconsistencies at the very early stages, right it is more cost effective.
This talk will give an overview of Educed's journey, from its founders' first steps to its latest achievements.
WWW: www.educed-emb.com/
6/6/2012, 11h30m DCC-FCUP Sala 3.
Formal methods in industry: Educed's path to make it happen
Orador: José Miguel Faria, Leading founder
Resumo:
After a three months period of highly successful customer validation in Silicon Valley, interacting with world leader companies in the Aeronatics, Space and Medical Devices domains, Educed is back in Portugal fully focused on maturing its flagship product, PROVA.
PROVA offers companies a solution for drastically reducing the effort and cost of delivering top quality high-integrity software. It provides mathematically powerfull techniques for analysing and validating the textual requirements of a system, identifying possible ambiguities, omissions, and inconsistencies at the very early stages, right it is more cost effective.
This talk will give an overview of Educed's journey, from its founders' first steps to its latest achievements.
WWW: www.educed-emb.com/