IMI/Publicaţii/CSJM/Ediţii/CSJM v.26, n.1 (76), 2018/

Implementation of the Composition-nominative Approach to Program Formalization in Mizar

Authors: Ievgen Ivanov, Artur Kornilowicz, Mykola Nikitchenko
Keywords: Formal methods, program semantics, semistructured data, formalization, proof assistant.


In this paper we describe an ongoing work on implementation of the composition-nominative approach to program formalization in Mizar proof assistant based on the first-order logic and axiomatic set theory. The further aim of this work is development of a formal verification tool for software which processes and communicates with complex forms of data.

Ievgen Ivanov, Mykola Nikitchenko
Taras Shevchenko National University of Kyiv, Ukraine
E-mail: ,
Artur Korni lowicz
University of Bia lystok, Poland


Adobe PDF document0.12 Mb