SDVS (State Delta Verification System): Program Verification System Development Fiscal Year 1986.
AEROSPACE CORP EL SEGUNDO CA LAB OPERATIONS
Pagination or Media Count:
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 Crockers 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 systems 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.
- Computer Programming and Software