Abstract
RP programs are imperative programs with parallelism and recursion and only a limited way of synchronizing parallel processes. The formal 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.
Thanks: This research was mainly done while the 2 authors were at the Leibniz-IMAG Lab. in Grenoble.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.
J. A. Bergstra and J. W. Klop. Process theory based on bisimulation semantics. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, LNCS 354, pages 50–122. Springer-Verlag, 1989.
J. C. M. Baeten and W. P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge Univ. Press, 1990.
J. Esparza. More infinite results. In Proc. Int. Workshop Verification of Infinite State Systems, Pisa, pages 4–20, August 1996.
O. Kouchnarenko. Sémantique des programmes récursifs-parallèles et méthodes pour leur analyse. Thèse de Doctorat, Univ. Joseph Fourier-Grenoble I, France, February 1997.
J. B. Kruskal. Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture. Trans. Amer. Math. Soc., 95:210–225, 1960.
O. Kouchnarenko and Ph. Schnoebelen. A model for recursive-parallel programs. In Proc. Int. Workshop Verification of Infinite State Systems, Pisa, pages 127–138, August 1996.
O. Kouchnarenko and Ph. Schnoebelen.Modèles formels pour les programmes récursifs-parallèles. In Proc. RENPAR'8, Bordeaux, pages 85–88, May 1996.
F. Moller. Infinite results. In Proc. CONCUR'96, Pisa, Italy, LNCS 1119, pages 195–216. Springer-Verlag, August 1996.
Y. Mamatov, V. Vasilchikov, S. Volchenkov, and V. Kurchidis. Multiprocessor computer system with dynamic parallelism. Technical Report 7160, VINITI, Moscow, Russia, September 1988.
Ph. Schnoebelen. On the analysis of RP schemes. Unpublished notes, November 1996.
V. Vasilchikov, V. Emielyn, V. Kurchidis, and Y. Mamatov. Recursive-parallel programming and work in RPMSHELL. IPVT RAN, Iaroslavl, Russia, 1994.
D. J. Walker. Bisimulations and divergence. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kushnarenko, O., Schnoebelen, P. (1997). A formal framework for the analysis of recursive-parallel programs. In: Malyshkin, V. (eds) Parallel Computing Technologies. PaCT 1997. Lecture Notes in Computer Science, vol 1277. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63371-5_6
Download citation
DOI: https://doi.org/10.1007/3-540-63371-5_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63371-6
Online ISBN: 978-3-540-69525-7
eBook Packages: Springer Book Archive