Í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.

Acetatos

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

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

• Alcino Cunha. An introduction to Alloy.

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

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

• Alcino Cunha. A perspective on model checking.

• J.N. Oliveira. Foundations of the PF relational calculus (31 slides)

• Ana Paiva. Model Based Testing.

• J. Visser. Software Analysis and Testing. Part 1 ; Part 2 ; Part 3

• J.N. Oliveira. PF-notation and Alloy: "Relational thinking'' at work (44 slides)

• L. S. Barbosa. Software architecture for reactive systems.

• L. S. Barbosa. Labeled transition systems.

• L. S. Barbosa. Introduction to process algebra.

• L. S. Barbosa. Logics for processes (I).

• L. S. Barbosa. Logics for processes (II).

• L. S. Barbosa. Time-critical systems and timed automata (I). Uppaal examples demo

• M. J. Frade. Formal Logic and Deduction Systems.

• M. J. Frade. Classical Propositional Logic.

• M. J. Frade. Classical First-Order Logic. (Exercícios em Coq.)

• M. J. Frade. Beyond First-Order Logic. (Exercícios em Coq.)

• M. J. Frade. The Curry-Howard Isomorphism. (Exercícios em Coq.)

• M. J. Frade. More About Coq. (Exercícios em Coq.)

• L. S. Barbosa. Time-critical systems and timed automata (II).

• L. S. Barbosa. Lamport protocol in Uppaal

• J. S. Pinto. Safety Verification with Frama-C / Jessie

• J. S. Pinto. Functional Verification with Frama-C / Jessie

• J. S. Pinto. Introduction to Formal Verification of Software

• J. S. Pinto. A logic for annotated programs

• J. S. Pinto. Generation of Verification Conditions

Exercícios e formulários

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

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

• L. S. Barbosa. PAS - exercises 1.

• L. S. Barbosa. PAS - exercises 2 (Uppaal).

• M. J. Frade. VFS - Exercícios de avaliação (Coq).

Software

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

Exemplos

• File System (.als)
• Eu sou o meu avô (.als)
• Barqueiro (.als)
• QuickCheck (.hs)

Provas de avaliação individual

• Módulo CSI (18-Fev): enunciado.
• Módulo AMT (18-Fev): enunciado, MPlayerMetrics.xls.