A Designer/Verifier’s Assistant



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.This paper describes a working computer program called the designer/verifier’s assistant, which is the initial prototype of such a system. The ...

Get Readings in Artificial Intelligence and Software Engineering now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.