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

Anything in here will be replaced on browsers that support the canvas element