A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices ⋆

Interactive systems with registers and voices (shortly, rv- systems) are a model for interactive computing obtained closing register machines with respect to a space-time duality transformation ("voices" are the time-dual counterparts of "registers"). In the same vain, AGAPIA v0.1, a structured programming language for rv-systems, is the space- time dual closure of classical while programs (over a specific type of data). Typical AGAPIA programs describe open processes located at various sites and having their temporal windows of adequate reaction to the environment. The language naturally supports process migration, structured interaction, and deployment of components on heterogeneous machines. In this paper a sound Hoare-like spatio-temporal logic for the verifica- tion of AGAPIA v0.1 programs is introduced. As a case study, a formal verification proof of a popular distributed termination detection protocol is presented.