Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

The C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is imp...

Full description

Bibliographic Details
Main Author: Dmitry A. Kondratyev
Format: Article
Language:English
Published: Yaroslavl State University 2021-12-01
Series:Моделирование и анализ информационных систем
Subjects:
deductive verification
c-lightver
cloud parallel programming system
symbolic method of verification of definite iterations
loop invariant
acl2
Online Access:https://www.mais-journal.ru/jour/article/view/1566

Internet

https://www.mais-journal.ru/jour/article/view/1566

Similar Items