Ementa: Conceitos básicos de lógica matemática e matemática discreta. Prova de correção de programas. Especificação e verificação formal de sistemas. Especificação e verificação de sistemas concorrentes e reativos. Verificação de modelos.
Bibliografia:
1.Ben-Ari, M., “Mathematical Logic for Computer Science”, Prentice-Hall, (1993);
2.Schneider, S., “Concurrent and Real-Time Systems. The CSP Approach”, John Wiley & Sons, (2000);
3.Clarke, E. M., Grumberg, O., Doron, A., Peled, D. A., “Model Checking”, The MIT Press, (1999);
4.Hoare, C. A. R., “Communicating Sequential Processes”, Prentice-Hall, (1985);
5.Nolt, J., Rohatyn, D., “Lógica”, Schaum McGraw?-Hill, Makron Books, (1991);
6.Roscoe, W., “The Theory and Practice of Concurrency”, Prentice Hall, (1998);