Computação Fiável e Segura

Departamento de Informática
Universidade da Beira Interior

Ano lectivo 2005/2006
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

Abordar os conceitos, os algoritmos, as técnicas e as ferramentas próprias à engenharia da fiabilidade (ou Métodos Formais) e à engehnaria da segurança (da informação).

4  Programa

5  Critérios de Avaliação

A avaliação será realizada por exame e por avaliação contínua. Listamos a seguir as diferentes componentes da avaliação.

5.1  Componente Ensino/Aprendizagem

5.2  Admissão e Avaliação por Exame

6  Material Pedagógico

Apontamentos apresentados e disponibilizados nas aulas. Aula de apresentação

Fichas práticas

7  Horário

Tipo de aula Horário Sala
Teórica Sexta-Feira das 9h00 às 11h00 6.03

8  Atendimento

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

9  Links úteis

References

[1]
Peter Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter C.7, pages 739–782. North-Holland, Amsterdam, 1977.

[2]
A. Arnold and I. Guessarian. Mathematics for Computer Science. Prentice-Hall, 1996.

[3]
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[4]
D. Bagley. The great computer language shootout. http://www.bagley.org/~doug/shootout

[5]
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.

[6]
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.

[7]
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.

[8]
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

[9]
D. Bjorner. Software Engineering 1 : Abstraction And Modelling. Springer Verlag, 2005.

[10]
D. Bjorner. Software Engineering 2: Specification Of Systems And Languages. Springer Verlag, 2005.

[11]
D. Bjorner. Software Engineering 3: Domains, Requirements, And Software Design. Springer Verlag, 2005.

[12]
S. Burris and H. Sankappanavar. A Course in Universal Algebra. Springer Verlag, 1981. http://www.cs.uu.nl/people/franka/ref

[13]
E. Chailloux, P. Manoury, and B. Pagano. Developing applications with objective caml. http://caml.inria.fr/oreilly-book, 2003.

[14]
Grumberg O. Clarke, E.M. and D Peled. Model Checking. MIT Press, 2000.

[15]
J. Cooke. Constructing correct software. Formal approaches to computing and information technology. Springer Verlag, 2005.

[16]
B. A. Davey and H. A. Priestley. Introduction to Lattices and Order: Second Edition. Cambridge University Press, 2002.

[17]
E. Gimenez. A tutorial on recursive types in Coq. http://coq.inria.fr/doc-eng.html

[18]
J-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1988.

[19]
Chris Hankin. Lambda Calculi: A Guide for Computer Scientists, volume 3 of Graduate Texts in Computer Science. Clarendon Press, Oxford, 1994.

[20]
J. W. Klop. Term rewriting systems. In S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 1–116. Oxford University Press, New York, 1992.

[21]
J. L. Krivine. Lambda-Calculus, Types and Models. Ellis Horwood, 1993.

[22]
J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Translation editor M. Hinchey.

[23]
H. R. Nielson and F. Nielson. Semantics with Applications. John Wiley & Sons, Chichester, 1993. http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html

[24]
H. R. Nielson, F. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.

[25]
L. Pequet. Programmation fonctionelle - introduction illustrée en objective caml. http://www-rocq.inria.fr/~pecquet/pro/teach/teach.html, 2002.

[26]
Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.

[27]
Benjamin C. Pierce, editor. Advanced Topics in Types and Programming Languages. MIT Press, 2005.

[28]
A. Pitts. Lecture notes on denotational semantics. University of Cambridge Computer Laboratory, 1999. http://www.cl.cam.ac.uk/Teaching/1998/DenoSema/dens.ps.gz

[29]
A. Pitts. Lecture notes on computation theory. University of Cambridge Computer Laboratory, 2002. http://www.cl.cam.ac.uk/Teaching/2002/CompTheory

[30]
I. Poernomo, J. Crossley, and M. Wirsing. Adapting Proofs-as-Programs, The Curry–Howard Protocol. Monographs in Computer Science. Springer Verlag, 2005.

[31]
F. Prost and G. Kahn. Checking mathematical facts with coq: Various examples of Coq proofs. http://coq.inria.fr/contribs-eng.html

[32]
K. Schneider. Verification of Reactive Systems. EATCS Series. Springer Verlag, 2004.

[33]
Coq Development Team. Documentation of the coq theorem prover. http://coq.inria.fr/doc-eng.html

[34]
Coq Development Team. Reference manual of the Coq theorem prover. http://coq.inria.fr/doc-eng.html

[35]
Coq Development Team. A tutorial of the Coq theorem prover. http://coq.inria.fr/doc-eng.html

[36]
OCaml Development Team. The Objective Caml system:Documentation and user's manual, 2002. http://caml.inria.fr/ocaml/htmlman/index.html

[37]
D. van Dalen. Logic and Structure. Springer Verlag, Berlin, Germany, 1983.

[38]
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.