Programação Certificada

No quadro actual, em que a segurança dos sistemas assume um papel determinante, torna-se fulcral a capacidade de produzir código certificado: o produto final de um projecto de software deixa de consistir exclusivamente em aplicações executáveis, sendo necessariamente acompanhado de certificados que asseguram que essas aplicações possuem propriedades desejadas, sejam elas funcionais ou de segurança. Por exemplo, pode ser imperioso que um programa cumpra uma determinada política que o impeça de aceder a recursos que lhe são vedados. A Verificação Formal é a actividade que pretende estabelecer que um sistema se comporta, efectivamente, de acordo com a sua especificação, ou que o seu comportamento apresenta certas propriedades, ou ainda que não apresenta defeitos. Por outro lado, a emergência de novas áreas de aplicação como a bioinformática e a criptografia relança o papel fundamental do estudo dos algoritmos e das suas propriedades nas ciências da computação.

A presente UCE responde precisamente a estes imperativos cruciais. Pretende-se estabelecer competências a dois níveis:

• Ao nível fundamental, pretende-se construír uma base sólida de conhecimentos, indispensáveis para a abordagem de alguns dos problemas mais sofisticados na área da Informática. Estes conhecimentos organizam-se em três áreas essenciais da Ciência da Computação: a Lógica e Semântica da Programação; os princípios das Linguagens de Programação; e o estudo dos Algoritmos e sua complexidade.

• Ao nível aplicado, esta UCE atribui competências na área da Verificação Formal de sistemas informáticos e na utilização de ferramentas de verificação (baseadas em modelos ou em inferência lógica), bem como na utilização de técnicas avançadas no domínio das linguagens de programação (nomeadamente as funcionais, que se prestam particularmente ao raciocínio sobre programas).

Coordenação Científica

• João Alexandre Saraiva
• José Bernardo Barros
• José Espirito Santo
• Jorge Sousa Pinto
• Luís Pinto
• Maria João Frade

Resultados de Aprendizagem

• Compreender os fundamentos da Teoria de Tipos, suas implicações nos sistemas de tipos de linguagens, e sua interpretação lógica; exprimir propriedades lógicas em sistemas de prova assistida, e conduzir demonstrações nesses sistemas.
• Conhecer as principais classes de complexidade e as relações elementares entre estas.
• Especificar, exprimir, e verificar a validade de propriedades (relativas à correcção ou outras) de sistemas de software, com recurso a ferramentas de prova assistida e verificadores de modelos.
• Aplicar técnicas avançadas de programação, nomeadamente funcional, para a resolução de problemas concretos.
• Reconhecer características dos problemas em áreas de aplicação diversas; utilizar algoritmos clássicos dessas áreas; analisar, comparar, e desenhar algoritmos.
• Desenvolver projectos integrados de desenvolvimento e verificação de software.

Módulos

A presente UCE organiza-se em torno de 3 módulos temáticos, articulados entre si por um Seminário e Projecto Integrado que garante, por um lado, complementar os temas abordados nos diversos módulos com palestras pontuais de professores e investigadores convidados; por outro lado, permite a experimentação e aplicação prática dos resultados da aprendizagem no contexto de um projecto integrado. Os módulos referidos são

• Fundamentos da Programação
• Verificação de Software
• Programação Avançada

Parcerias

• Dep. Matemática, UM