|
Article information
2020 , Volume 25, ¹ 5, p.91-106
Kondratyev D.A., Promsky A.V.
Towards verification of scientific and engineering programs. The CPPS project
Nowadays, when formal fundamentals of program verification are well studied, researchers concentrate their efforts on domain-specific methods for various classes of programs. However, it seems that the field of scientific and engineering applications still lacks attention. We would like to contribute to filling this gap through the development of the Cloud Parallel Programming System (CPPS). The goal of this project is to create a parallel programming system for Sisal programs. Deductive verification of Sisal programs is one the of important subgoals. Since the Cloud Sisal language is built on the basis of loop expressions, their axiomatic semantics is the basis of Hoare’s logic for the Sisal language. The Cloud Sisal loop expressions, array construction expressions and array element replacement expressions enable efficiently executable computational or engineering mathematics programs. Thus, we believe that our axiomatic semantics for these types of expressions may present an interesting result.
[full text]
Keywords: Cloud Sisal, deductive verification, Cloud-Sisal-kernel, C-lightVer, cloud parallel programming system, ACL2, loop invariant
doi: 10.25743/ICT.2020.25.5.008
Author(s):
Kondratyev Dmitry Aleksandrovich
Position: Junior Research Scientist
Office: A.P. Ershov Institute of Informatics Systems Siberian Branch of the Russian Academy of Sciences
Address: 630090, Russia, Novosibirsk, 6, Acad. Lavrentyev pr.
E-mail: apple-66@mail.ru
SPIN-code: 4318-8908Promsky Alexey Vladimirovich
PhD.
Position: Scientific Secretary
Office: A.P. Ershov Institute of Informatics Systems Siberian Branch of the Russian Academy of Sciences
Address: 630090, Russia, Novosibirsk, 6, Acad. Lavrentyev pr.
Phone Office: (383) 3307068
E-mail: promsky@iis.nsk.su
SPIN-code: 6871-9688 References:
1. Kasyanov V., Kasyanova E. Methods and system for cloud parallel programming. Proceedings of the 21st International Conference on Enterprise Information Systems, Heraklion, 2019. Setubal: SciTePress; 2019: 623–629.
2. Kasyanov V., Kasyanova E. A system of functional programming for supporting of cloud supercomputing. WSEAS Transactions on Information Science and Applications. 2018; 15(9):81–90.
3. H¨ahnle R, Huisman M. Deductive software verification: From pen-and-paper proofs to industrial tools. Lecture Notes in Computer Science. 2019; (10000):345–373.
4. Kondratyev D., Promsky A. Proof strategy for automated Sisal program verification. Lecture Notes in Computer Science. 2019; (11771):113–120.
5. Kondratyev D., Promsky A. Correctness of proof strategy for the Sisal program verification. Proceedings of 2019 International Multi-Conference on Engineering, Computer and Information Sciences (SIBIRCON), Novosibirsk, 2019. IEEE; 2019: 641–646.
6. Kondratyev D., Maryasov I., Nepomniaschy V. The automation of C program verification by the symbolic method of loop invariant elimination. Automatic Control and Computer Sciences. 2019; 53(7):653–662.
7. Hoare C.A.R. An axiomatic basis for computer programming. Communications of the ACM. 1969; 12(10):576–80.
8. Apt K.R., Olderog E.-R. Fifty years of Hoare’s logic. Formal Aspects of Computing. 2019; 31(6):751–807.
9. Moore J.S. Milestones from the pure Lisp theorem prover to ACL2. Formal Aspects of Computing. 2019; 31(6):699–732.
10. Kasyanov V. Sisal 3.2: functional language for scientific parallel programming. Enterprise Information Systems. 2013; 7(2):227–236.
11. Nepomniaschy V. Symbolic method of verification of definite iterations over altered data structures. Programming and Computer Software. 2005; (31):1–9.
12. Kondratyev D.A. The extension of the C-light project using symbolic verification method of definite iterations. Computational Technologies. Special Issue: “XVII All-Russian Conf. of Young Scientists on Mathematical Modeling and Information Technology”. 2017; (22):44–59. (In Russ.).
13. Attali I., Caromel D., Wendelborn A. A formal semantics and an interactive environment for Sisal. International Series in Software Engineering. 1996; (2):229–256.
14. Swamy N., Hrit,cu C., Keller C., Rastogi A., Delignat-Lavaud A., Forest S., Bhargavan K., Fournet C., Strub P.-Y., Kohlweiss M., Zinzindohoue J.-K., Zanella-B´eguelin S. Dependent types and multi-monadic effects in F*. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, USA, 2016. New York: ACM; 2016: 256–270. Available at: https: //www.fstar-lang.org/papers/mumon/paper.pdf
15. Myreen M.O., Gordon M.J.C. Transforming programs into recursive functions. Electronic Notes in Theoretical Computer Science. 2009; (240):185–200.
16. Volkov G., Mandrykin M., Efremov D. Lemma functions for Frama-C: C programs as proofs. Proceedings of 2018 Ivannikov Ispras Open Conference (ISPRAS), Moscow, 2018. IEEE; 2018: 31–38.
17. Efremov D., Mandrykin M., Khoroshilov A. Deductive verification of unmodified Linux Kernel library functions. Lecture Notes in Computer Science. 2018; (11245):216–234.
Bibliography link:
Kondratyev D.A., Promsky A.V. Towards verification of scientific and engineering programs. The CPPS project // Computational technologies. 2020. V. 25. ¹ 5. P. 91-106
|
