• automata
• model-checking
• nominal

This thesis investigates and proposes models for programming and verifying adaptive software at different abstraction levels.
First, we design the kernel of a programming language, endowed with primitives for programming the adaptation to different working environments.
We provide the language with a type and effect system that allows us to statically prove properties of the behaviour of the program when plugged in different execution environments.
Then we extend our language to program the use of the resources currently available in the environment.
In this case, the identity and the number of resources is unknown a-priori.
The previous analysis technique needs to be extended to capture the behaviour of these programs.
We exploit nominal techniques in the literature to propose novel automata models that represent the behaviour and the properties of programs that use an unbounded number of unknown resources as (regular and context-free) set of traces.
The theoretical properties of these automata are investigated and related with static program verification.
We prove that we are able to check regular properties of the usage patterns of the resources when resource reuse is inhibited.