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...

Descrizione completa

Dettagli Bibliografici

Autore principale:	Dmitry A. Kondratyev
Natura:	Artigo
Lingua:	Inglês
Pubblicazione:	Yaroslavl State University 2021-12-01
Serie:	Моделирование и анализ информационных систем
Soggetti:	deductive verification c-lightver cloud parallel programming system symbolic method of verification of definite iterations loop invariant acl2
Accesso online:	https://www.mais-journal.ru/jour/article/view/1566
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!