|
UNIVERSIDADE DO ESTADO DO RIO DE JANEIRO
|
| UNIDADE: INSTITUTO POLITÉCNICO | ||
| DEPARTAMENTO: DEPARTAMENTO DE MODELAGEM COMPUTACIONAL | ||
| DISCIPLINA: Interpretação Abstrata | ||
| CARGA HORÁRIA: 60 | CRÉDITOS: 4 | CÓDIGO: IPRJ01-10790 |
| MODALIDADE DE ENSINO: Presencial | TIPO DE APROVAÇÃO: Nota e Frequência | |
| STATUS | CURSO(S) / HABILITAÇÃO(ÕES) / ÊNFASE(S) |
| Eletiva Restrita | IPRJ - Engenharia de Computação (versão 1) |
| Eletiva Definida | IPRJ - Engenharia de Computação (versão 1) |
| TIPO DE AULA | CRÉDITO | CH SEMANAL | CH TOTAL |
| Teórica | 4 | 4 | 60 |
| TOTAL | 4 | 4 | 60 |
OBJETIVO(S):
Fornecer os fundamentos de Interpretação Abstrata.
EMENTA:
Elementos da teoria de pontos fixos. Conexões de Galois. Abstrações exatas de pontos fixos. Abstração de semântica de traços. Aproximação construtiva de pontos fixos. Inferência de tipos para Cálculo Lambda através da Interpretação Abstrata. Correção e Completude de métodos de provas de programas. Reticulados de Interpretações Abstratas. Exemplos.
BIBLIOGRAFIA: 1. P. Cousot. Types as abstract interpretations. POPL 1997. ACM Press, New York, NY, U.S.A.
2. P. Cousot et R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL 1977. ACM Press, New York, NY, USA.
3. P. Cousot et R. Cousot. Systematic design of program analysis frameworks. POPL 1979. ACM Press, New York, NY, U.S.A.
4. P. Cousot et R. Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2(4):511--547, August 1992.
5. Flemming Nielson, Hanne Riis Nielson, Chris Hankin: Principles of Program Analysis. Springer (Corrected 2nd printing, 452 pages, ISBN 3-540-65410-0), 2005.