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

Cezara Dragoi, Gheorghe Stefanescu

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…