Computer Science Colloquium

Analyzing Properties of Systems

Aaron Bradley
Stanford University

Tuesday, April 17th 11:45 a.m.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185

Colloquium Information:


Richard Cole, (212) 998-3119


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.

Refreshments will be served

top | contact