Computer Science Colloquium
Analyzing Properties of Systems
Tuesday, April 17th 11:45 a.m.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html
Richard Cole email@example.com, (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
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
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
| contact firstname.lastname@example.org