Computação Fiável

Departamento de Informática
Universidade da Beira Interior

Ano lectivo 2012/2013



Esta página no formato pdf

1  Novidades

Contents

2  Docentes

Simão Melo de Sousa (regente) - Gabinete 3.17 - Laboratório 6.10 - Bloco VI

3  Objectivos

4  Competências por adquirir

Os alunos deverão

5  Programa

6  Critérios de Avaliação

A avaliação avaliará a aprendizagem teóricas e prática dos conceitos introduzidos. Como tal, esta será constituida por provas escrita e por resoluções de exercícios práticos.

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  Software

Proof Assistants : COQ

Design by contract - Deductive Program Verification : Principalmente why3, mas também Frama-C

Model checking: Uppaal

E se houver tempo

Atelier B

9  Material Pedagógico e Referências Bibliográficas

10  Horário

Tipo de aulaHorárioSala
TeóricaSexta-Feira das 14h00 às 16h006.13
PráticaSexta-Feira das 16h00 às 18h006.13

11  Atendimento

Horário
Sexta 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]
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. edition, 2011.
[3]
H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984.
[4]
H.P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and T.S.E Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117–310. Oxford University Press, New York, 1992.
[5]
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.
[6]
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
[7]
D. Bjorner. Software Engineering 1 : Abstraction And Modelling. Springer Verlag, 2005.
[8]
D. Bjorner. Software Engineering 2: Specification Of Systems And Languages. Springer Verlag, 2005.
[9]
D. Bjorner. Software Engineering 3: Domains, Requirements, And Software Design. Springer Verlag, 2005.
[10]
E.M. Clarke, O. Grumberg, and D Peled. Model Checking. MIT Press, 2000.
[11]
J. Cooke. Constructing correct software. Formal approaches to computing and information technology. Springer Verlag, 2005.
[12]
E. Gimenez. A tutorial on recursive types in Coq. http://coq.inria.fr/doc-eng.html
[13]
Chris Hankin. Lambda Calculi: A Guide for Computer Scientists, volume 3 of Graduate Texts in Computer Science. Clarendon Press, Oxford, 1994.
[14]
K. Lano and H. Haugthon. Specification in B: An Introduction using the B Toolkit. Imperial College Press, 1996.
[15]
David Makinson. Sets, Logic and Maths for Computing. Springer Publishing Company, Incorporated, 1 edition, 2008.
[16]
J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Translation editor M. Hinchey.
[17]
H. R. Nielson, F. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.
[18]
B. C. Pierce. Types and Programming Languages. MIT Press, 2002.
[19]
B. C. Pierce, editor. Advanced Topics in Types and Programming Languages. MIT Press, 2005.
[20]
S. Schneider. The B-Method: An Introduction. Cornerstones of Computing series. Palgrave, 2001.
[21]
Coq Development Team. Reference manual of the Coq theorem prover. http://coq.inria.fr/doc-eng.html
[22]
Coq Development Team. A tutorial of the Coq theorem prover. http://coq.inria.fr/doc-eng.html
[23]
R. D. Tennent. Specifying Software. A Hands-On Introduction. Cambridge University Press, 2002.
[24]
A. S. Troelstra and H. Schwichtenberg. Basic proof theory. Cambridge University Press, New York, NY, USA, 1996.
[25]
D. van Dalen. Logic and Structure. Springer Verlag, Berlin, Germany, 1983.
[26]
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.