Cover Image

Correctness Property Proof for the Banking System for Money Transfer Payments

The method for properties proof for parallel programs running multiple-instance interleaving with shared memory was applied in order to prove the correctness property of the banking system for remittances payments. The task was stated, transitional system was built for the model with simplified stat...

Full description

Saved in:

Bibliographic Details
Date:	2018
Main Authors:	Ostapovska, Yu.A., Panchenko, T.V., Polishchuk, N.V., Kartavov, M.O.
Format:	Article
Language:	Ukrainian
Published:	PROBLEMS IN PROGRAMMING 2018
Subjects:	software correctness safety property proof concurrent program interleaving invariant IPCL composition-nominative languages formal verification UDC 004.415.52
Online Access:	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/187
Tags:	Add Tag No Tags, Be the first to tag this record!
Journal Title:	Problems in programming
Download file:

Institution

Problems in programming

Similar Items

Peterson’s algorithm Total correctness proof in IPCL
by: Zhygallo, A.A.
Published: (2018)

Equivalence of two parallel execution systems
by: Panchenko, T.V., et al.
Published: (2018)

Correctness Property Proof for the Banking System for Money Transfer Payments
by: Yu. A. Ostapovska, et al.
Published: (2016)

Models of concurrent program running in resource constrained environment
by: Rahozin, D.V.
Published: (2020)

Formal verification of deep neural networks
by: Panchuk, B.O.
Published: (2024)

Toward software artifacts ecosystem
by: Sydorov, N.A.
Published: (2021)

Description model of programming style ecosystem
by: Sydorov, N.A., et al.
Published: (2020)

Basics of programming in the context of software engineering
by: Sydorov, М.О.
Published: (2019)

The translator of Petri-object model visual programming language
by: Dyfuchyn, А.Yu.
Published: (2022)

Logics of quasiary predicates of quantifier-equational level
by: Nikitchenko, M.S., et al.
Published: (2015)

The definition of formal languages in the meta language of normal forms of knowledge
by: Kurgaev, A.F., et al.
Published: (2018)

Jupyter Notebook: a system for interactive scientific computing
by: Yakimchik, A. I.
Published: (2019)

Representation of monadic effects in the non-monadic form
by: Shevchenko, R.S.
Published: (2024)

The software tool of constructive-synthesizing modeling
by: Shynkarenko, V.I., et al.
Published: (2024)

An approach of intelligent searching of information in texts
by: Chebanuyk, O.V.
Published: (2023)

50 years of software engineering
by: Sydorov, N.A.
Published: (2019)

Context term calculus for rewriting systems
by: Shevchenko, R.S.
Published: (2018)

Semantics and pragmatics of programming language ASAMPL
by: Sulema, Y.S., et al.
Published: (2020)

Algebraic modeling in international and local service logistical systems
by: Letychevskyi, O.O., et al.
Published: (2021)

TermWare3 – term rewriting system, based on context-term calculus
by: Shevchenko, R.S., et al.
Published: (2019)

Survey on modern tools and methods of formal models verification
by: Kolchin, A.V., et al.
Published: (2015)

Development of integrated system of scientific periodicals based on the OJS
by: Kudim, K.A., et al.
Published: (2017)

Sound interface design for blind PC users
by: Ruvinskaya, V.M., et al.
Published: (2015)

Towards ecosystem research in the software engineering
by: Sydorov, M.O.
Published: (2024)

Embedding a family of logic languages with custom monadic unification in Scala
by: Shevchenko, R.S., et al.
Published: (2024)

DS-theory. Scientific aspects and prospects for development
by: Kolesnyk, V.G.
Published: (2018)

Software engineering ontologies categorization
by: Sydorov, N.A., et al.
Published: (2018)

About one Approach for the Verification of Algebraic Computations
by: Lvov, M.S.
Published: (2025)

Regression testing: techniques and future research directions
by: Moroz, H.B., et al.
Published: (2025)

Static method of consistency and completeness checking in formal model of distributed software systems
by: Kolchin, A.V., et al.
Published: (2025)

Traversal of arbitrary sequences of UCM symbolic transitions for test generation
by: Guba, A.A.
Published: (2025)

The grammar of Petri-object model visual programming language
by: Dyfuchyn, А.J., et al.
Published: (2022)

Analysis of suitable converter for the implementation of drive system in solar photovoltaic panels
by: Themozhi, G., et al.
Published: (2024)

About geological theory
by: Gordienko, V.V.
Published: (2022)

Component of programming. Theory and implementation
by: Lavrischeva, K.M.
Published: (2015)

Features of building recommendation systems based on neural network technology using multithreading
by: Komleva, N.O., et al.
Published: (2023)

ІНКРЕМЕНТНИЙ ЦИФРОВИЙ КВАЗІІДЕАЛ ІНТЕГРАТОР ЗАЯВКИ ПОПЕРЕДНЬОГО ПОТОКУ ОЦІНКИ КЕРУЮЧОЇ ІНДУКЦІЙНОЇ МАШИНИ
by: Ustun, O., et al.
Published: (2008)

COLONIAL PICOFOSSIL'S OF PRECAMBRIAN HYME-NOPHACOIDES ROBLOT 1964: STAGES OF THEIR REPLICATION AS THE BASIC ARGUMENT OF THEIR BIOGENIC VERIFICATION
by: LOPUKHIN, A. S., et al.
Published: (2011)

DS-theory. Research of R-data division factors in order to generate applied algorithms. Part 1
by: Kolesnyk, V.G.
Published: (2017)

Protection of information objects from intentional collisions of inspection characteristics in error-correcting codes
by: Mаtоv, O. Y., et al.
Published: (2016)