×

Problem-oriented program verification system “SPEKTR”. (English. Russian original) Zbl 0655.68019

Cybernetics 23, No. 6, 757-765 (1987); translation from Kibernetika 1987, No. 6, 31-37 (1987).
The paper describes a program verification system SPEKTR. It is based on Hoare’s calculus extended by special rules for for-loops (called loop invariant elimination). In the theorem proving part a ‘conditional system of reductions’ is used. The system consists of an analyzer for source programs (in modified Pascal), a generator of correctness conditions and an interactive theorem prover containing a decision procedure for Presburger arithmetic, a conditional reductor, a case analysis module and an inductive proof module.
Reviewer: H.Müller

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

SPEKTR
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] V. A. Nepomnyashchii, ?Practical methods of program verification,? Kibernetika, No. 2, 21?28 (1984).
[2] V. A. Nepomnyashchii, ?Elimination of loop invariants during program verification,? Programmirovanie, No. 3, 3?13 (1985).
[3] V. A. Nepomnyashchii, ?On problem-oriented program verification,? Programmirovanie, No. 1, 3?12 (1986).
[4] V. A. Nepomnyashchii, ?Proving correctness of linear algebra programs,? Programmirovanie, No. 4, 63?72 (1982).
[5] S. G. Vorob’ev, ?On application of conditional term substitution systems for program verification,? Programmirovanie, No. 4, 3?14 (1986).
[6] C. A. R. Hoare, ?Proof of correctness of data representation,? in: Data in Programming Languages [Russian translation], Mir, Moscow (1982), pp. 54?67.
[7] R. E. Shostak, ?On the sup-inf method for proving Presburger formulas,? J. ACM,24, No. 4, 529?543 (1977). · Zbl 0423.68052
[8] R. E. Shostak, ?A practical decision procedure for arithmetic with function symbols,? J. ACM,26, No. 2, 351?360 (1979). · Zbl 0496.03003
[9] G. Huet and D. C. Oppen, ?Equations and rewrite rules. A survey,? Formal Language Theory: Perspectives and Open Problems, Academic Press, NY (1980), pp.349?406.
[10] G. A. Kucherov, ?Term substitution systems,? Preprint [in Russian], No. 601, VTs SO AN SSSR, Novosibirsk (1985).
[11] S. G. Vorob’ev, ?On building in decidable fragments of arithmetic for term rewriting systems,? in: Compiling and Program Design [in Russian], VTs SO AN SSSR, Novosibirsk (1986), pp. 91?97.
[12] S. G. Vorob’ev, ?Inductive definitions and proofs in conditional term rewriting systems,? in: Problems of Improving Design, Testing, Verification, and Debugging of Programs, abstracts of papers at All-Union Conf. [in Russian], Vol. 1, VTs Latv. Gos. Univ., Riga (1986), pp. 73?75.
[13] A. N. Bezdushnyi and A. A. Sulimov, ?Implementation of the basic language of a program verification system using the compiler construction system SUPER,? in: Programming Theory and Tools of Describing Parallelism of Discrete Systems [in Russian], VTs SO AN SSSR, Novosibirsk (1985), pp. 29?37.
[14] A. A. Sulimov, ?Functional specifications of a compiler,? in: Compiling and Transformation of Programs [in Russian], VTs SO AN SSSR, Novosibirsk (1984), pp. 137?150.
[15] N. Wirth, Algorithms + Data Structures = Programs [Russian translation], Mir, Moscow (1985).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.