Work number - M 96 ALLOWED TO PARTICIPATE
Peschanenko V.S., Blinov I.O., Klionov D.M.
Khersonstateuniversity
Optimization of mathematical and program software, which is used for proving of insertional models properties, is presented in this work.
Overview of proving properties, modern systems and methods of verification of formal models are given. Satisfiability checking algorithm, forward and backward predicate transformers are presented.
Algorithm of interleaving reduction in symbolic insertional models is created. Concepts of necessary and sufficient conditions of permutability, including definitions of static and dynamic permutability, are presented. Algorithm of reachability of user defined states are generalized. Algorithm of separation formulae for specializations is described. Abstract predicate transformer, which is invariant of data structures, is presented. Algorithm of concretize of symbolic traces, which is help to create concrete traces, is defined. Partial evaluations algorithms are provided for insertion models. Existence of backward behavior in full extended enriched algebra of behavior is proved. REM language is optimized. Time efficiency of non-deterministic strategy of rewriting is proved in term of REM language. Effective algorithm of translation of APLAN code to C++ code is obtained.
System VRS is briefly described as industrial system where obtained results are used. System of Provable Programming and constraint insertion models are presented.
Publications.46 relatedpapershadbeenpublished,25 papersin scientificaljournals(total volume14 а.а., 11 papersinbibliographic databaesDBLP, GoogleScholar, EI-Compendex, MathematicalReviews, SCImago, Scopus, 1 paper‒ inforeign journalindexed by bibliographic databaseРІНЦ), 6 papers‒ injournals, 4 areindexedbyDBLP, GoogleScholar(total volume4 а.а.), 8 reports thesis’s(total volume1,5 а.а.), 4 inventors’ certificates.
Версія для друку