Geodesic
Methods for deductive verification of C code using AstraVer Toolset
Prikladnaya Diskretnaya Matematika. Supplement, no. 15 (2022), pp. 80-90

Voir la notice de l'article provenant de la source Math-Net.Ru

Some practical methods for deductive verification of C code for compliance with ACSL specifications are described. For verification, Astraver Toolset based on the Frama-C platform is used. Approbation of these methods was carried out during the verification of access control module in PARSEC security subsystem of secure operating system Astra Linux Special Edition. For example, the method of global ghost variables allows monitoring shared memory, this is helpful for verification of certain functions. There is also a specification validation method that can help find out if the written specification is lacking. Thanks to these methods, it is possible to simplify function specifications, reduce labour intensity and speed up deductive verification. Examples of the use of the proposed methods are given.
Keywords: deductive software verification, AstraVer Toolset
Mots-clés : ACSL, Frama-C, Astra Linux. 
@article{PDMA_2022_15_a20,
     author = {A. O. Kokorin and S. D. Tievskiy and P. N. Devyanin},
     title = {Methods for deductive verification of {C} code using {AstraVer} {Toolset}},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {80--90},
     publisher = {mathdoc},
     number = {15},
     year = {2022},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2022_15_a20/}
}
TY  - JOUR
AU  - A. O. Kokorin
AU  - S. D. Tievskiy
AU  - P. N. Devyanin
TI  - Methods for deductive verification of C code using AstraVer Toolset
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2022
SP  - 80
EP  - 90
IS  - 15
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDMA_2022_15_a20/
LA  - ru
ID  - PDMA_2022_15_a20
ER  - 
%0 Journal Article
%A A. O. Kokorin
%A S. D. Tievskiy
%A P. N. Devyanin
%T Methods for deductive verification of C code using AstraVer Toolset
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2022
%P 80-90
%N 15
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDMA_2022_15_a20/
%G ru
%F PDMA_2022_15_a20
A. O. Kokorin; S. D. Tievskiy; P. N. Devyanin. Methods for deductive verification of C code using AstraVer Toolset. Prikladnaya Diskretnaya Matematika. Supplement, no. 15 (2022), pp. 80-90. http://geodesic.mathdoc.fr/item/PDMA_2022_15_a20/