Sumários
Model Checking I
5 Novembro 2025, 16:30 • Antónia Lopes
- Introduction
- Modelling sequential programs in Promela
- Specifying properties with assertions in Promela
- Verifying sequential programs with Spin
Exercises Dafny&Classes
29 Outubro 2025, 18:30 • Antónia Lopes
Exercises4 (Dafny&Classes): 4.1 a, b, c, 4.2 a, b, c, 4.4 a, b (partially)
Design by contract: Contracts for Data Abstractions
29 Outubro 2025, 16:30 • Antónia Lopes
- Design by contract: Contracts for Data Abstractions (cont'd)
- Dynamic frames and idioms for expressing representation frames
- Property-based specifications
- Observers, Producers and Mutators
- 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
Não houve aula (dia investigação)
22 Outubro 2025, 18:30 • Antónia Lopes
Não houve aula (dia investigação)