Sumários

Model Checking II

21 Novembro 2017, 18:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Modelling concurrent systems with Promela

    • Concurrency

    • Shared memory

    • Linear Temporal Logic

Model Checking I

14 Novembro 2017, 18:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Introduction
  • Sequential programming in Promela
  • Verification of sequential programs

Extended Static Checking

7 Novembro 2017, 16:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • History, static analysis versus runtime verification
  • Soundness and completness
  • Architecture of Esc/Java2
  • The Bag tutorial
  • Limitations that we need to be aware of
  • Tracing a warning in the source code
  • Counterexamples
  • Exceptions

Type Specifications III

31 Outubro 2017, 18:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Model-based Specifications in JML

Type Specifications II

24 Outubro 2017, 18:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Behavioural subtyping
  • Model-based Specifications in JML