Accession Number : ADA184338

Title :   SDVS (State Delta Verification System): Program Verification System Development Fiscal Year 1986.

Descriptive Note : Final rept.,

Corporate Author : AEROSPACE CORP EL SEGUNDO CA LAB OPERATIONS

Personal Author(s) : Marcus,Leo G

PDF Url : ADA184338

Report Date : 01 Jul 1987

Pagination or Media Count : 14

Abstract : This report describes the progress made in the State Delta Verification System (SDVS) research and development effort for fiscal year 1986. The long-term goal of the field of program verification is to be able to prove the correctness of any program with respect to its (correct) specification. Existing program verification systems can be classified according to their intended domain of application, degree of user interaction, and choice of specification language. SDVS 5 is the current version of a program verification project that essentially started in Crocker's thesis and has progressed since then in capability of proof, ease of user interface, and complexity of applications actually tackled. SDVS is a highly interactive proof checker for proofs of microcode correctness. SDVS 5 runs on the Symbolics Lisp Machine version 6. It consists of three modules: the kernel and user interface (6000 lines of lisp code), the simplifier (14,000 lines of lisp code), and the translator from the ISPS machine description language to state deltas (4000 lines of lisp code). The kernel directs the symbolic execution and checks the validity of the dynamic proof commands. The simplifier encodes the system's knowledge of static domains and allows the user to create and prove lemmas for future use. The translator converts descriptions written in an expanded ISPS to the internal state delta language.

Descriptors :   *COMPUTER PROGRAM VERIFICATION, *ERROR CORRECTION CODES, USER NEEDS, INTERACTIONS, SEMANTICS, SPECIFICATIONS, INSTRUCTIONS, VALIDATION

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE