Authors: Ievgen Ivanov, Artur Kornilowicz, Mykola Nikitchenko
Keywords: Formal methods, program semantics, semistructured data, formalization, proof assistant.
– 0.12 Mb
Keywords: Formal methods, program semantics, semistructured data, formalization, proof assistant.
Abstract
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
E-mail:
Taras Shevchenko National University of Kyiv, Ukraine
E-mail: , Artur Korni lowicz
University of Bia lystok, Poland
E-mail:
Fulltext
– 0.12 Mb
