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

Simple item page
dc.creatorDragoi, Cezara
dc.creatorStefanescu, Gheorghe
dc.date2008-10-19
dc.date.accessioned2026-07-07T10:11:33Z
dc.date.available2026-07-07T10:11:33Z
dc.descriptionInteractive 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 verification of AGAPIA v0.1 programs is introduced. As a case study, a formal verification proof of a popular distributed termination detection protocol is presented.
dc.description21 pages, 8 figures, Invited submission for WADT'08 LNCS Proceedings
dc.identifierhttps://arxiv.org/abs/0810.3332
dc.identifierhttp://arxiv.org/abs/0810.3332
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/171895
dc.subjectProgramming Languages
dc.subjectLogic in Computer Science
dc.subjectF.1.2; F.3; D.2.4; D.3.2
dc.titleA sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices
dc.typetext

Files

Collections

arXiv