As the complexity of and the dependence on engineered systems rises,
correctness becomes ever more important. Verification aims to prove or
to disprove that a system's implementation meets its specification. A
specification asserts a set of properties that should hold on all
executions of the system. Two areas of research are fundamental to
verification: invariant generation and decision procedures. In this
talk, I describe progress in both.
I first present a strategy for letting properties guide an invariant
generation procedure, a form of static analysis. I then exhibit two
instances of the strategy. The first augments generation of affine
inequality invariants to be property-directed. For the second instance,
I introduce a procedure for generating clausal invariants of
finite-state systems such as hardware circuits and show how to make it
property-directed.
Arrays are ubiquitous data structures in software and in hardware
specifications. I present a decision procedure for a fragment of a
theory of arrays that allows some quantification. Besides being
expressive, this fragment is interesting because it lies on the edge of
decidability: natural and simple extensions produce undecidable
fragments.
Finally, I briefly discuss my work with Zohar Manna on developing a new
undergraduate course at Stanford. Our course and accompanying
forthcoming text, both entitled "The Calculus of Computation", cover
first-order logic; decision procedures; and software specification,
verification, and analysis.