Methods for deductive verification of C code using AstraVer Toolset

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.