A Formal Framework for the Analysis of Recursive-Parallel Programs
by O. Kushnarenko, Ph. Schnoebelen
Abstract:
RP programs are imperative programs with parallelism and recursion and only a limited way of synchronizing parallel processes. The format framework we propose here combines (1) a formal operational model of abstract programs (or RP schemes), (2) a set of decision methods for the analysis of RP schemes, (3) a formal operational model for the interpreted programs, and (4) translation results stating how some behavioural properties of the concrete programs can be correctly checked on the corresponding scheme.
Keywords: theory, semantics of concurrency, automated verification of programs, infinite state systems
Source:
O. Kushnarenko, P. Schnoebelen, A Formal Framework for the Analysis of Recursive-Parallel Programs. In V. Malyshkin (ed.),
Parallel Computing Technologies: Proceedings of the 4th International Conference,
Lect. Notes in Comp. Sci., Vol. 1277, Springer, 1997, pp. 45-59
