Institutul de Matematică şi Informatică "Vladimir Andrunachievici"
Universitatea de Stat din MoldovaRO EN
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.
– 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
Contents
- On Nontrivial Covers and Partitions of Graphs by Convex Sets
- Bounds for the Independence Number in k-Step Hamiltonian Graphs
- Vertex weighted Laplacian Energy of union of graphs
- Parallel algorithm to find Bayes-Nash solution to the bimatrix informational extended game
- Implementation of the Composition-nominative Approach to Program Formalization in Mizar
- Finite automata over magmas: models and some applications in Cryptography
- Annotation on PhD Thesis
- About International Conference MITI2018
