Registration Number
0219U000269,
0116U004732
, R & D reports
Title
Methods of computer algebra and insertion modeling in static analysis systems and software verification.
popup.stage_title
Head
Lvov Michael,
Registration Date
24-01-2019
Organization
Kherson State Teacer Training University
popup.description2
The contents of the library of algorithms of computer algebra of the static programs analysis are formed. A new method to prove the invariance of the system of linear inequalities and termination of linear definite iterative loops for imperative programs was present . Was present an algorithm for constructing the canonical forms of logical formulas off data types. The functional requirements and the structure of Web-resource of research group for international scientific collaboration and of Web-resource of algorithms library of computer algebra of static program analysis was defined. Requirements for the system of verification of formal program models are formed. The functional specification and architecture of the insertion system are determined. The prototype of an insertion machine has been developed.
Product Description
popup.authors
Барановська О.В.
Блинов І.О.
Вінник М.О.
Кльонов Д.М.
Кушнір Н.О.
Мельник Д.Г.
Мельник Д.Г.
Надєєва В.В.
Немченко Д.О.
Осіпова Н.В.
Песчаненко В.С.
Полторацький М.Ю.
Приймак К.С.
Тарасіч Ю.Г.
Черненко І.Є.
Шишко Н.В.
Шміло О.В.
Шорнік В.М.
popup.nrat_date
2020-04-02
