Implementation of the Composition-nominative Approach to Program Formalization in Mizar
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 whic...
Main Authors: | Ievgen Ivanov, Artur Kornilowicz, Mykola Nikitchenko |
---|---|
Format: | Article |
Language: | English |
Published: |
Vladimir Andrunachievici Institute of Mathematics and Computer Science
2018-05-01
|
Series: | Computer Science Journal of Moldova |
Subjects: | |
Online Access: | http://www.math.md/files/csjm/v26-n1/v26-n1-(pp59-76).pdf |
Similar Items
-
Proving Properties of Programs on Hierarchical Nominative Data
by: Ievgen Ivanov, et al.
Published: (2016-12-01) -
Type-alpha DPLs
by: Arkoudas, Konstantine
Published: (2004) -
Formal Verification of Robot Rotary Kinematics
by: Guojun Xie, et al.
Published: (2023-01-01) -
Blockchain-Based Authentication Protocol Design from a Cloud Computing Perspective
by: Zhiqiang Du, et al.
Published: (2023-05-01) -
Compositional lexical networks: a case study of the English spatial adjectives
by: Worthing, D
Published: (2021)