Índice do material disponível:

Bibliografia

• Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. CUP, 2007.

• Christel Baier, Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.

• Daniel Jackson. Software abstractions: logic, language, and analysis. MIT Press, 2006.

• C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)

• Robin Milner. Communicating and Mobile Systems: The Pi Calculus. CUP, 1999.

• J.N. Oliveira. Transforming Data by Calculation. In volume 5235 of LNCS, pages 134-192, 2008.

• J.N. Oliveira. Extended static checking by calculation using the pointfree transform. In A. Bove et al., editor, volume 5520 of LNCS, pages 195-251. Springer-Verlag, 2009.

• Pitts A. M. Lecture Notes on Semantics of Programming Languages. Univ Cambridge, 1997-2002 (disponível online aqui)

Divulgação

• Daniel Jackson. Dependable Software by Design. Scientific American, Junho 2006.

• Daniel Jackson. A Direct Path to Dependable Software. DOI:10.1145/1498765.1498787, Abril 2009.

• David Parnas. Really Rethinking 'Formal Methods'. IEEE Computer 43(1), 28–34 (2010).

Acetatos

• J.N. Oliveira. Data type invariants: starting where (static) type checking stops (24 slides)

• J.N. Oliveira. Pre / post-conditions -- starting where (pure) functions stop (29 slides)

• J.N. Oliveira. PF transform: when everything becomes a relation (43 slides)

• Alcino Cunha. An introduction to Alloy. Versão definitiva.

• J.N. Oliveira. PF transform: conditions and coreflexives for ESC (28 slides)

• J.N. Oliveira. “Theorems for free”: a (calculational) introduction (27 slides)

• J.N. Oliveira. PF-transform: using Galois connections to structure relational algebra (35 slides)

• Alcino Cunha. A perspective on model-checking.

• Joost Visser. Software Analysis and Testing (parte 1, parte 2, parte 3, parte 4).

• Luís S. Barbosa. Labelled transition systems (revised notes, 2011.04.02).

• Luís S. Barbosa. Introduction to CCS.

• Luís S. Barbosa. Hennessy-Milner logic.

• Luís S. Barbosa. The modal mu-calculus.

• Luís S. Barbosa. Introduction to mCRL2 (and mini-project).

• Luís S. Barbosa. An introduction to Reo.

Exemplos

• Alloy: eu sou o meu próprio avô, sistema de ficheiros, e barqueiro.

• Alloy: noDuplicates.zip

Exercícios

• Colectânea de exercícios de testes sobre Alloy.

• Exercícios sobre lógica temporal e model-checking.

• J.N. Oliveira. (2010.11.07) CSI Module — List of classroom exercises

(23 exercises)

• Formulário do Cálculo Relacional (7 págs)

• Luís S. Barbosa. Exercises on labelled transition systems.

• Luís S. Barbosa. Exercises on CCS.

Software

• Alloy Analyzer
• Uppaal
• Coq
• Frama-C
• VDM/Overture

Repositórios

• Repositório de ferramentas da associação FME.

Enunciados de provas de avaliação individual

• Módulo CSI (10-Fev): enunciado.
• Módulo CSI (21-Jul): enunciado .
• Módulo VFS (20-Jun): enunciado.
• Módulo VFS (21-Jul): enunciado.