Sumários

Exercises about Model Checking with Spin

13 Novembro 2024, 18:30 • Antónia Lopes

Model Checking I

13 Novembro 2024, 16:30 • Antónia Lopes

Model Checking

  • Introduction
  • Modelling sequential programs in Promela
  • Specifying properties with assertions in Promela
  • Verifying sequential programs with Spin

Exercises with Dafny : Model and Property based Specifications for classes

6 Novembro 2024, 18:30 • Antónia Lopes

Design by contract: Contracts for Data Abstractions

6 Novembro 2024, 16:30 • Antónia Lopes

  • Design by contract: Contracts for Data Abstractions (cont'd)
    • Model-based specifications for Object Types
      • Using built-in Immutable Types as models
      • Abstraction functions vs Abstraction Fields
    • Datatypes in Dafny
    • Model-based specifications for Datatypes
  • Design by contract in Java 
    • JML
    • Deductive verification and runtime verification

Exercises in Dafny: Dbc for Classes

30 Outubro 2024, 18:30 • Antónia Lopes