|
Conteúdos programáticos |
Introdução: problemática, contexto, história e lugar dos Métodos Formais na Engenharia Informática e na Eng. de Software.
Especificar, Modelar e Analisar SIs: Especificação formal, máquina abstracta de estados, lógica de Hoare. Semântica operacional, semântica denotacional
Especificar e Demonstrar Propriedades de SIs: verificação de modelo, sistemas de prova automática, sistemas de ajuda a prova.
Especificar e Derivar Implementações: extracção de programas, refinamento
Especificar e Transformar: interpretação abstracta.
|
|
Bibliografia principal |
J.B. Almeida, M.J. Frade, J.S. Pinto, and S. Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification, volume 103 of Undergraduate Topics in Computer Science. Springer-Verlag, first edition, 307 p. 52 illus, 2011.
Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001.
J. Cooke. Constructing correct software. Formal approaches to computing and information technology. Springer Verlag, 2005.
Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Serie. Springer Verlag, 2004.
J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Translation editor M. Hinchey.
R. D. Tennent. Specifying Software. A Hands-On Introduction. Cambridge University Press, 2002.
|