Formal methods of parallel software design automation

Doroshenko, AY
Yatsenko, OA
Dopov. Nac. akad. nauk Ukr. 2020, 6:15-20
Section: Information Science and Cybernetics
Language: English

Formal methods and software tools of automated design and synthesis of parallel programs are proposed. The developed facilities use the language based on the Glushkov system of algorithmic algebras intended for a highlevel and natural linguistic representation of algorithms and apply rewriting rules technique to transform programs. The tools also use the method of syntactically correct algorithm scheme design which eliminates syntax errors during the construction of algorithms and programs. The approach is illustrated on developing the parallel N-body simulation program for the executing on a graphics processing unit.

Keywords: algebra of algorithms, automated design, formal methods, graphics processing unit, parallel computation, term rewriting

1. Doroshenko, A., & Shevchenko, R. (2006). A rewriting framework for rule-based programming dynamic applications. Fundamenta Informaticae, 72(1-3), pp. 95-108.
2. Andon, P. I., Doroshenko, A. Yu., Zhereb, K. A., & Yatsenko, O. A. (2018). Algebra-algorithmic models and methods of parallel programming. Kyiv: Akademperiodyka.
3. Doroshenko, A. Yu., & Yatsenko, O. A. (2020). Formal and adaptive methods for automation of parallel programs construction. (unpublished manuscript)
4. Butler, R. W. (2001). What is formal methods? Retrieved from
5. Flener, P. (2002). Achievements and prospects of program synthesis. In A. C. Kakas & F. Sadri (Eds.). Computational Logic: Logic Programming and Beyond. LNCS (Vol. 2407, pp. 310-346). Berlin: Springer.
6. Gulwani, S. (2010). Dimensions in program synthesis. Proc. of the 12th Int. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (pp. 13-24). New York: ACM.
7. Nvidia CUDA technology (n.d.). Retrieved from
8. Prusov, V. & Doroshenko, A. (2018). Computational techniques for modeling atmospheric processes. Hershey, PA: IGI Global.
9. Aarseth, S. J. (2003). Gravitational N-body simulations: Tools and algorithms. Cambridge: Cambridge University Press.
10. Makino, J., & Aarseth, S. J. (1992). On a Hermite integrator with Ahmad-Cohen. Publications of the Astronomical Society of Japan, 44, pp. 141-151.