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

Ivanov Ievgen; Kornilowicz Artur; Nikitchenko Mykola

Conţinutul numărului revistei

Articolul precedent

Articolul urmator

898

Ultima descărcare din IBN:
2019-02-28 20:17

Căutarea după subiecte
similare conform CZU

004.9+519.6 (3)

Informatică aplicată. Tehnici bazate pe calculator cu aplicații practice (438)

Matematică computațională. Analiză numerică. Programarea calculatoarelor (123)

SM ISO690:2012

IVANOV, Ievgen, KORNILOWICZ, Artur, NIKITCHENKO, Mykola. Implementation of the Composition-nominative Approach to Program Formalization in Mizar. In: Computer Science Journal of Moldova, 2018, nr. 1(76), pp. 59-76. ISSN 1561-4042.

EXPORT metadate:
Google Scholar
Crossref
CERIF

DataCite
Dublin Core

Computer Science Journal of Moldova

Numărul 1(76) / 2018 / ISSN 1561-4042 /ISSNe 2587-4330

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

CZU: 004.9+519.6

Pag. 59-76

Ivanov Ievgen¹, Kornilowicz Artur², Nikitchenko Mykola¹

¹ Taras Shevchenko National University of Kyiv,
² University of Bialystok

Disponibil în IBN: 4 mai 2018

Descarcă PDF

Rezumat

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.

Cuvinte-cheie
Formal methods,

program semantics, semistructured data, formalization, proof assistant.

Cerif XML Export

<?xml version='1.0' encoding='utf-8'?>
<CERIF xmlns='urn:xmlns:org:eurocris:cerif-1.5-1' xsi:schemaLocation='urn:xmlns:org:eurocris:cerif-1.5-1 http://www.eurocris.org/Uploads/Web%20pages/CERIF-1.5/CERIF_1.5_1.xsd' xmlns:xsi='http://www.w3.org/2001/XMLSchema-instance' release='1.5' date='2012-10-07' sourceDatabase='Output Profile'>
<cfResPubl>
<cfResPublId>ibn-ResPubl-61949</cfResPublId>
<cfResPublDate>2018-03-31</cfResPublDate>
<cfVol>76</cfVol>
<cfIssue>1</cfIssue>
<cfStartPage>59</cfStartPage>
<cfISSN>1561-4042</cfISSN>
<cfURI>https://ibn.idsi.md/ro/vizualizare_articol/61949</cfURI>
<cfTitle cfLangCode='EN' cfTrans='o'>Implementation of the Composition-nominative Approach to Program Formalization in Mizar</cfTitle>
<cfKeyw cfLangCode='EN' cfTrans='o'>Formal methods; program semantics; semistructured
data; formalization; proof assistant.</cfKeyw>
<cfAbstr cfLangCode='EN' cfTrans='o'><p>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.</p></cfAbstr>
<cfResPubl_Class>
<cfClassId>eda2d9e9-34c5-11e1-b86c-0800200c9a66</cfClassId>
<cfClassSchemeId>759af938-34ae-11e1-b86c-0800200c9a66</cfClassSchemeId>
<cfStartDate>2018-03-31T24:00:00</cfStartDate>
</cfResPubl_Class>
<cfResPubl_Class>
<cfClassId>e601872f-4b7e-4d88-929f-7df027b226c9</cfClassId>
<cfClassSchemeId>40e90e2f-446d-460a-98e5-5dce57550c48</cfClassSchemeId>
<cfStartDate>2018-03-31T24:00:00</cfStartDate>
</cfResPubl_Class>
<cfPers_ResPubl>
<cfPersId>ibn-person-46088</cfPersId>
<cfClassId>49815870-1cfe-11e1-8bc2-0800200c9a66</cfClassId>
<cfClassSchemeId>b7135ad0-1d00-11e1-8bc2-0800200c9a66</cfClassSchemeId>
<cfStartDate>2018-03-31T24:00:00</cfStartDate>
</cfPers_ResPubl>
<cfPers_ResPubl>
<cfPersId>ibn-person-56442</cfPersId>
<cfClassId>49815870-1cfe-11e1-8bc2-0800200c9a66</cfClassId>
<cfClassSchemeId>b7135ad0-1d00-11e1-8bc2-0800200c9a66</cfClassSchemeId>
<cfStartDate>2018-03-31T24:00:00</cfStartDate>
</cfPers_ResPubl>
<cfPers_ResPubl>
<cfPersId>ibn-person-35052</cfPersId>
<cfClassId>49815870-1cfe-11e1-8bc2-0800200c9a66</cfClassId>
<cfClassSchemeId>b7135ad0-1d00-11e1-8bc2-0800200c9a66</cfClassSchemeId>
<cfStartDate>2018-03-31T24:00:00</cfStartDate>
</cfPers_ResPubl>
</cfResPubl>
<cfPers>
<cfPersId>ibn-Pers-46088</cfPersId>
<cfPersName_Pers>
<cfPersNameId>ibn-PersName-46088-3</cfPersNameId>
<cfClassId>55f90543-d631-42eb-8d47-d8d9266cbb26</cfClassId>
<cfClassSchemeId>7375609d-cfa6-45ce-a803-75de69abe21f</cfClassSchemeId>
<cfStartDate>2018-03-31T24:00:00</cfStartDate>
<cfFamilyNames>Ivanov</cfFamilyNames>
<cfFirstNames>Ievgen</cfFirstNames>
</cfPersName_Pers>
</cfPers>
<cfPers>
<cfPersId>ibn-Pers-56442</cfPersId>
<cfPersName_Pers>
<cfPersNameId>ibn-PersName-56442-3</cfPersNameId>
<cfClassId>55f90543-d631-42eb-8d47-d8d9266cbb26</cfClassId>
<cfClassSchemeId>7375609d-cfa6-45ce-a803-75de69abe21f</cfClassSchemeId>
<cfStartDate>2018-03-31T24:00:00</cfStartDate>
<cfFamilyNames>Kornilowicz</cfFamilyNames>
<cfFirstNames>Artur</cfFirstNames>
</cfPersName_Pers>
</cfPers>
<cfPers>
<cfPersId>ibn-Pers-35052</cfPersId>
<cfPersName_Pers>
<cfPersNameId>ibn-PersName-35052-3</cfPersNameId>
<cfClassId>55f90543-d631-42eb-8d47-d8d9266cbb26</cfClassId>
<cfClassSchemeId>7375609d-cfa6-45ce-a803-75de69abe21f</cfClassSchemeId>
<cfStartDate>2018-03-31T24:00:00</cfStartDate>
<cfFamilyNames>Nikitchenko</cfFamilyNames>
<cfFirstNames>Mykola</cfFirstNames>
</cfPersName_Pers>
</cfPers>
</CERIF>