Carga horária da disciplina: 4 horas/aula

Professor(es) em 2024-1

Turma 11

Professor: Rodrigo Geraldo Ribeiro - www | e-mail Horários: Segunda-feira (17h10 - 18h50) Quarta-feira (17h10 - 18h50)

Objetivos

Ementa

Lógica de primeira ordem: sintaxe, semântica e raciocínio algébrico; Procedimentos de decisão para lógica proposicional; Lógica intuicionista e teoria de tipos; Lógica temporal e verificadores de modelos; Lógicas de Hoare e de Separação; Indução e co-indução para verificação de programas.

Conteúdo Programático

- Revisão de lógica de primeira ordem: sintaxe, semântica e raciocínio algébrico.
- Procedimentos de decisão para lógica proposicional.
        - O algoritmo DPLL e modelagem de problemas usando SAT-solvers.
- Lógica intuicionista e o cálculo lambda
        - O isomorfismo de Curry-Howard e uso de assistentes de provas baseados em teoria de tipos.
- Lógicas temporais LTL e CTL
        - Sintaxe e semântica.
        - Uso de verificadores de modelos para prova de propriedades expressas em lógicas temporais.
- Lógicas de Hoare e de Separação
        - Provas de propriedades sobre programas imperativos.
        - Verificação de programas que manipulam ponteiros em C.
- Uso de assistentes de provas para demonstração de propriedades por indução e co-indução.

Bibliografia

- HUTH, Michael; RYAN, Mark. Lógica em ciência da computação: modelagem e argumentação sobre sistemas. 2. ed. Rio de Janeiro: LTC, 2008.
- BERTOT, Yves; CASTÉRAN, P. Interactive theorem proving and program development - Coq'Art : the calculus of inductive constructions. Berlin, New York: Springer, 2004.
- MITCHELL, John C. Foundations for programming languages. Cambridge: MIT Press, 2000.

Bibliografia complementar

- CLARKE, Edmund M; GRUMBERG, Orna; PELED, Doron A. Model checking. London: MIT Press, 1999.
- BRADLEY, Aaron R; MANNA, Zohar. The Calculus of computation: decision procedures with applications to verification. Berlin: Springer, 2007.
- HINDLEY, J. Roger; SELDIN, Jonathan P. Lambda-calculus and combinators: an introduction. Cambridge: Cambridge University Press, 2008.
- ENDERTON, Herbert B. A mathematical introduction to logic. 2. ed. New York: Academic Press, 2001.
- PIERCE, Benjamin C. Types and programming languages. Cambridge, Mass.: MIT Press, 2002.