Thursday, April 19, 2007
4:15 pm
B17 Upson Hall

Computer Science
Spring 2007

Aaron Bradley
Stanford University

Analyzing Properties of Systems

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.