TWiki · Education/MFES1112 · Material

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

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.

(Mais bibliografia a adicionar à medida que as aulas prossigam)

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

M.J. Frade. Logic-lesson4.pdf (30 slides, 8 pages) 2011. Coq demo: lesson4.v

M.J. Frade. Logic-lesson5.pdf (71 slides, 18 pages) 2012. Coq demo: CoqBrief.v

M.J. Frade. Logic-lesson6.pdf (55 slides, 14 pages) 2012. Coq demo: IndDefs.v, CaseStudy.v

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

J.N. Oliveira. Pre / post-conditions -- starting where (pure) functions stop (31 slides) (updated 2011)

J.N. Oliveira. PF transform: when everything becomes a relation (54 slides) (updated: 8-12-2011)

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

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

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

(Mais acetatos a adicionar à medida que as aulas prossigam)

L. S. Barbosa. A course roadmap for 2011-12 (updated: 11-02-2012)
L. S. Barbosa. Project (part 1) (updated: 17-01-2012)
L. S. Barbosa. Project (part 2, variant A) (updated: 24-01-2012)
L. S. Barbosa. Project (part 2, variant B) (updated: 24-01-2012)
L. S. Barbosa. Project (part 2, variant C) (updated: 24-01-2012)
L. S. Barbosa. Lecture 1 (updated: 8-12-2011)
L. S. Barbosa. Lecture 2 (updated: 8-12-2011)
L. S. Barbosa. Lecture 3 (updated: 17-01-2012)
L. S. Barbosa. Lecture 4 (updated: 17-01-2012)
L. S. Barbosa. Lecture 5 (updated: 10-02-2012)
L. S. Barbosa. TPSession1 (updated 24-01-2012)
L. S. Barbosa. TPSession2 (updated: 10-02-2012)

David Garlan. Formal Modeling and Analysis of Software Architecture: Components, Connectors, and Events, Springer LNCS (2804), 2004. (updated: 8-12-2011)
Ian Gorton. Essential Software Architecture (table of contents and chapter 1), Springer 2006. (updated: 8-12-2011)
Colin Striling. Modal and temporal logics for processes, Springer LNCS (1043), 1996. (updated: 17-01-2012)
P. Blackburn, M. Rijke, I. Venema. Modal Logic (table of contents and chapter 1), CUP 2001. (updated: 17-01-2012)
F. Arbab. F. Arbab Inaugural Lecture at Leiden, Leiden University 2005. (updated: 10-02-2012)
F. Arbab. Abstract Behavior Types: a foundation model for components and their composition, SCP, 2005. (updated: 10-02-2012)
C. Baier et al. Modeling Component Connectors in Reo by Constraint Automata, SCP, 2006. (updated: 10-02-2012)
D. Clarke, D. Costa, F. Arbab. Connector colouring I: Synchronisation and context dependency, SCO, 2007. (updated: 10-02-2012)