OPERATIONAL SEMANTICS FOR LYaPAS | Applied Discrete Mathematics. Supplement. 2015. № 8.

HomeIssuesOPERATIONAL SEMANTICS FOR LYaPAS | Applied Discrete Mathematics. Supplement. 2015. № 8.

OPERATIONAL SEMANTICS FOR LYaPAS

The development of the operational semantics for LYaPAS is considered. The following two applications are possible: the proof of the complex-element references correctness by abstract interpretation method and the creation of a certified compiler.

Download file
Counter downloads: 275

Keywords

операционная семантика, ЛЯПАС, абстрактная интерпретация, верифицирующий транслятор, operational semantics, LYaPAS, abstract interpretation, certified compiler

Authors

NameOrganizationE-mail
Zhukovskaja A. O.Tomsk State Universityzhuka157@yandex.ru
Stefantsov D. A.Tomsk State Universityd.a.stefantsov@isc.tsu.ru
Всего: 2

References

The Coq Proof Assistant page. https://coq.inria.fr/
The CompCert page. http://compcert.inria.fr/
Besson F., Cachera D., Jensen T., and Pichardie D. Certified static analysis by abstract interpretation // Foundations of Security Analysis and Design. 2009. No. 5705. P. 223-257.
Агибалов Г. П., Липский В. Б., Панкратова И. А. О криптографическом расширении и его реализации для Русского языка программирования. // Прикладная дискретная математика. 2013. №3. С. 93-105.
OPERATIONAL SEMANTICS FOR LYaPAS | Applied Discrete Mathematics. Supplement. 2015. № 8.

OPERATIONAL SEMANTICS FOR LYaPAS | Applied Discrete Mathematics. Supplement. 2015. № 8.

Download full-text version
Counter downloads: 1755