Computação Fiável

Departamento de Informática
Universidade da Beira Interior

Ano lectivo 2007/2008

Esta página no formato pdf, no formato ps

1  Novidades

Contents

2  Docentes

Simão Melo de Sousa (regente) - Gabinete 4.3.

3  Objectivos

4  Competências por adquirir

Os alunos deverão

5  Programa

6  Critérios de Avaliação

A avaliação será realizada por uma prova escrita e por avaliação contínua.
Fraudes
A equipa docente gostaria de realçar que qualquer tipo de fraude em qualquer dos itens desta disciplina implica a reprovação automática do aluno faltoso, podendo ainda vir a ser alvo de processo disciplinar. Listamos a seguir as diferentes componentes da avaliação.

6.1  Componente Ensino/Aprendizagem Prática

6.2  Componente Ensino/Aprendizagem Teórica

6.3  Admissão e Avaliação por Exame

7  Datas Importantes

8  Material Pedagógico e Referências Bbliográficas

9  Horário

Tipo de aula Horário Sala
Teórica Quarta-Feira das 17h00 às 19h00 6.02
Prática Quinta-Feira das 16h00 às 18h00 6.14

10  Atendimento

Horário
Quarta-Feira das 16h00 às 18h00
Quinta-Feira das 11h00 às 13h00
ou por mail (medida anti spam, retire os UUU): desousaUUU@UUUdi.ubi.pt.

References

[1]
J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.
[2]
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.
[3]
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. http://www-sop.inria.fr/lemme/Yves.Bertot/coqart.html
[4]
D. Bjorner. Software Engineering 1 : Abstraction And Modelling. Springer Verlag, 2005.
[5]
D. Bjorner. Software Engineering 2: Specification Of Systems And Languages. Springer Verlag, 2005.
[6]
D. Bjorner. Software Engineering 3: Domains, Requirements, And Software Design. Springer Verlag, 2005.
[7]
E.M. Clarke, O. Grumberg, and D Peled. Model Checking. MIT Press, 2000.
[8]
J. Cooke. Constructing correct software. Formal approaches to computing and information technology. Springer Verlag, 2005.
[9]
E. Gimenez. A tutorial on recursive types in Coq. http://coq.inria.fr/doc-eng.html
[10]
K. Lano and H. Haugthon. Specification in B: An Introduction using the B Toolkit. Imperial College Press, 1996.
[11]
J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Translation editor M. Hinchey.
[12]
H. R. Nielson, F. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.
[13]
B. C. Pierce. Types and Programming Languages. MIT Press, 2002.
[14]
B. C. Pierce, editor. Advanced Topics in Types and Programming Languages. MIT Press, 2005.
[15]
S. Schneider. The B-Method: An Introduction. Cornerstones of Computing series. Palgrave, 2001.
[16]
Coq Development Team. Reference manual of the Coq theorem prover. http://coq.inria.fr/doc-eng.html
[17]
Coq Development Team. A tutorial of the Coq theorem prover. http://coq.inria.fr/doc-eng.html
[18]
R. D. Tennent. Specifying Software. A Hands-On Introduction. Cambridge University Press, 2002.
[19]
G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing series. MIT Press, Cambridge, Massachusetts, February 1993.



Enviar comentários e dúvidas para (retire os UUU) : desousaUUU@UUUdi.ubi.pt
This document was translated from LATEX by HEVEA.