A Designer/Verifier´s Assistant

Author

Moriconi, Mark S.

Author_Institution

Computer Science Laboratory, SRI International

Issue

4

fYear

1979

fDate

7/1/1979 12:00:00 AM

Firstpage

387

Lastpage

401

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

Automated program verifier; automated programmer assistance; design of incremental systems; effects of incremental changes; incremental program design and verification; maintenance; program design; program specifications; program verification; proofs of programs; question answering; Contracts; Drain avalanche hot carrier injection; Error correction; File systems; Induction generators; Operating systems; Programming profession; Proposals; Prototypes; Software maintenance; Automated program verifier; automated programmer assistance; design of incremental systems; effects of incremental changes; incremental program design and verification; maintenance; program design; program specifications; program verification; proofs of programs; question answering;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/TSE.1979.234206

Filename

1702644