The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs

The C-lightVer system for the deductive verification of C programs is being developed at the IIS SB RAS. Based on the two-level architecture of the system, the C-light input language is translated into the intermediate C-kernel language. The meta generator of the correctness conditions receives the...

Popoln opis

Bibliografske podrobnosti

Principais autores:	Dmitry A. Kondratyev, Alexei V. Promsky
Format:	Artigo
Jezik:	Inglês
Izdano:	Yaroslavl State University 2019-12-01
Serija:	Моделирование и анализ информационных систем
Teme:	deductive verification semantic label error localization c-lightver acl2 metavcg definite iteration proof strategy
Online dostop:	https://www.mais-journal.ru/jour/article/view/1273
Oznake:	Označite Brez oznak, prvi označite!