Skip to main content


Weitere Artikel dieser Ausgabe durch Wischen aufrufen

01.12.2019 | Ausgabe 7/2019

Automatic Control and Computer Sciences 7/2019

The Automation of C Program Verification by the Symbolic Method of Loop Invariant Elimination

Automatic Control and Computer Sciences > Ausgabe 7/2019
D. A. Kondratyev, I. V. Maryasov, V. A. Nepomniaschy
Wichtige Hinweise
Translated by E. Glushachenkova


In the deductive verification of programs written in the imperative programming languages, the generation and proving of the verification conditions corresponding to loops are of particular complexity, as each of them must be provided with an invariant, whose construction is often a challenge. As a rule, the methods for the synthesis of loop invariants have a heuristic character, which complicates their application. An alternative is the symbolic loop invariant elimination method proposed by V.A. Nepomniaschy in 2005. Its idea is to represent a loop body in the form of a special replacement operation under certain constraints. Such an operation in the symbolic form expresses the loop effect, which allows introducing an inference rule for the loops without invariants into axiomatic semantics. This work is the further development of this method. It extends the proposed method of mixed axiomatic semantics for the verification of C-light programs. This extension incorporates the method for the verification of iterations over changeable arrays with the possible exit from the loop body in C-light programs. The method contains the inference rule for iterations without loop invariants. This rule has been implemented in the verification condition generator, which is a part of the automated system for the verification of C-light programs. To perform automated verification in the used ACL2 system, two algorithms, one of which generates the replacement operation in the ACL2 language, and the second generates the auxiliary lemmas resulting in the successful automated proof of the obtained verification conditions in the ACL2 system have been developed and implemented. The application of the above mentioned methods and algorithms is illustrated with an example.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Über diesen Artikel

Weitere Artikel der Ausgabe 7/2019

Automatic Control and Computer Sciences 7/2019 Zur Ausgabe