Material disponível ou a disponibilizar:

Bibliografia

• Daniel Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.

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

• J.B. Almeida, M.J. Frade, J.S. Pinto, and S. Melo de Sousa. Rigorous Software Development: An Introduction to Program Verification. Springer, 2011.

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

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

Outros textos

• J.N. Oliveira. Program Design by Calculation. Departamento de Informática, Universidade do Minho. Capítulo segundo deste livro em preparação.

Acetatos

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

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

• Alcino Cunha. An introduction to Alloy. Acetatos ligeiramente desactualizados no que respeita à modelação de sistemas dinâmicos.

• J.N. Oliveira. PF transform: when everything becomes a relation (57 slides) (last update: Oct-2012)

• J.N. Oliveira. “Theorems for free”: a (calculational) introduction (29 slides) (last update: Nov-2012)

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

• Alcino Cunha. Alloy: Under the Hood. Acetatos sobre semântica de lógica relacional, sistema de tipos e model finding. Para quem preferir código a notação matemática, pode consultar este programa em Haskell que implementa a semântica e o sistema de tipos.

• Alcino Cunha. A perspective on model checking. Acetatos sobre modelação, especificação e verificação de sistemas reactivos: estruturas de Kripke, redes de Petri, lógica temporal (LTL e CTL), verificação de modelos por enumeração exaustiva do espaço de estados e simbólica, ordered binary decision diagrams.

• J.N. Oliveira. Alloy meets the AoP: “relational thinking” at work (versão completa: 71 slides)

• J.N. Oliveira. PF-transform: using Galois connections to structure relational algebra (versão completa: 81 slides)

• M.J. Frade. Propositional Logic and SAT solvers.

• M.J. Frade. First-Order Logic and SMT.

• M.J. Frade. SMT solvers.

• Iago Abal. Applying SMT to problem solving. (Exemplos)

• M.J. Frade. Propositions-as-types analogy and the Coq proof assistant. (Coq file: lessonCoq1.v)

• M.J. Frade. Programming and Proving in Coq. (Coq file: lessonCoq2.v)

• L.S. Barbosa. Introduction to the PAS module.

• L.S. Barbosa. Part 1: Components as coalgebras (slides, texts, library).

• L.S. Barbosa. Part 2 (a): Coordination in reo (slides).

• José Proença. Part 2 (b): Runtime Reo (slides) (examples).

• Tool. Part 2 (c): Reo (tools & demos).

• Papers. Part 2 (d): Reo (reference & discussion).

• L.S. Barbosa. Parts 1 and 2: Open Exercises.

• L.S. Barbosa. Part 3 (a): Process-oriented architectural design (slides).

• Tool. Part 3 (b): mCRL2 (process algebra & logics).

• L.S. Barbosa. Part 3 (c): Interactive and probabilistic behaviour (slides)

• L.S. Barbosa. Part 3 (d): IMC tools & Stochastic Reo (zip).

• Papers. Part 3 (e): Stochastic constraints (reference & discussion).

• L.S. Barbosa. Part 3 (f): Timed behaviour and UPPAAL (slides)

• G. Voutsadakis (invited lecturer) Seminar on Measuring inconsistency.

Divulgação

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

• Eric Bouwers, Joost Visser, Arie van Deursen. Getting What You measure. Communications of the ACM (CACM) 55(7):54-59, July 2012.

• J.N. Oliveira. Towards Formal Software Development in VS.NET. MSDN Seminars - 14/16th of May, 2002, Porto & Lisbon.

• Leslie Lamport. Why We Should Build Software Like We Build Houses. Wired, 2013.

Exemplos

• Alloy
  • Eu sou o meu próprio avô. Versão inglesa da charada. Versão brasileira sugerida pelo Thiago Mendonça.
  • Book estático
  • Book dinâmico com global state idiom
  • Book dinâmico com local state idiom
  • Book dinâmico com local state idiom, operações como predicados
  • Book dinâmico com local state idiom, operações como eventos
  • Book dinâmico com local state idiom, operações como eventos, frame conditions ao estilo de Reiter
  • Book dinâmico com local state idiom, operações como predicados, traços com ordering
  • Book dinâmico com local state idiom, operações como eventos, traços com ordering
  • Farmer estático
  • Farmer dinâmico com local state idiom, operações como eventos, traços com ordering
  • Modelo do jogo Move the Box. Permite modelar e resolver níveis específicos. Para visionar os traços use este theme. Sugestão do Daniel Murta.
  • Exclusão mútua com semáforos
  • Exclusão mútua com o algoritmo de Dekker
  • Redes de Petri elementares. Incluindo exemplo de exclusão mútua com semáforos. Para visionar os traços use este theme.
• SMV
  • Exclusão mútua com semáforos
  • Exclusão mútua com o algoritmo de Dekker
  • Modelo que distingue F G p de AF AG p (com atribuições ou sistema de transição explícito)
• VFS
  • DPLL recursivo (em Haskell). Autor: Victor Miraldo.

Exercícios e formulários

• Exercícios sobre Alloy.
• Exercícios sobre Model Checking.
• Formulário de Álgebra Relacional (por cortesia de um colega)

Enunciados de provas de avaliação individual

• Teste sobre Alloy.
• Teste de CSI (com correcção)
• Exame de recurso de CSI

Módulo de VFS

• Trabalho sobre SMT-solvers.
• Material sobre Verificação Dedutiva / ACSL / Jessie
• Ficha de exercícios em Coq.
• Material sobre Verificação Automática / CMBC
• Trabalho Prático sobre Verificação Dedutiva

Ferramentas

• Alloy Analyzer
• NuSMV
• SPIN
• Frama-C
• Uppaal
• SMT-LIB - The Satisfiability Modulo Theories Library
• SATLIB - The Satisfiability Library
• The Coq Proof Assistant
• VDM/Overture

Vídeos

• Why model?
  • Intelligent Citizens of the World
  • Thinking More Clearly
  • Using Models to Decide, Strategize, and Design

Repositórios

• Repositório de ferramentas da associação FME.
• Repositório de padrões de especificação de lógica temporal.