A Designer/Verifier's Assistant

1 July 1979

journal article
Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering

Vol. SE-5 (4) , 387-401
https://doi.org/10.1109/tse.1979.234206

Abstract

Since developing and maintaining formally verified programs is an incremental activity, one is not only faced with the problem of constructing specifications, programs, and proofs, but also with the complex problem of determining what previous work remains valid following incremental changes. A system that reasons about changes must build a detailed model of each development and be able to apply its knowledge, the same kind of knowledge an expert would have, to integrate new or changed information into an existing model.

Keywords

This publication has 10 references indexed in Scilit:

Debugging Ada Tasking Programs
IEEE Software, 1985
The Interlisp Programming Environment
Computer, 1981
Initial Report on a Lisp Programmer's Apprentice
IEEE Transactions on Software Engineering, 1978
The programmer's workbench—a machine for software development
Communications of the ACM, 1977
A Verification System for JOCIT/J3 Programs (Rugged Programming Environment - RPE/2)
Published by Defense Technical Information Center (DTIC) ,1977
Proof techniques for hierarchically structured programs
Communications of the ACM, 1977
Gypsy
Published by Association for Computing Machinery (ACM) ,1977
An interactive program verification system
IEEE Transactions on Software Engineering, 1975
Towards a programming apprentice
IEEE Transactions on Software Engineering, 1975
Verifying programs by algebraic and logical reduction
Published by Association for Computing Machinery (ACM) ,1975