Problem-oriented knowledge bases and their application in the program verification system SPEKTR. The notion of the knowledge base is discussed within the framework of the problem-oriented approach to the program verification. A knowledge base consists of axioms represented by generalized condition term rewriting rules, strategies of their application, and decision procedures. The standard form of axioms is extended by conditions in premises and in the built-in, case-based reasoning. A survey of knowledge bases of sorting and compiling programs is given. The verification system SPEKTR is described, where the evidence of correctness is automatically shown with the use of knowledge bases.
Keywords for this software
References in zbMATH (referenced in 3 articles , 2 standard articles )
Showing results 1 to 3 of 3.
- Nepomnyashchij, V. A.; Sulimov, A. A.: Problem-oriented knowledge bases and their application in the program verification system SPEKTR (1997)
- Nepomnyashchij, V. A.; Sulimov, A. A.: Verification of linear algebra programs in the SPEKTR system (1992)
- Nepomnyashchij, V. A.; Vorob’ev, S. G.; Sulimov, A. A.: Problem-oriented program verification system “SPEKTR” (1987)