There is a signup schedule for this event.

Speaker Name/Affiliation: Aaron Bradley Stanford University

Da

te/Time: Tuesday March 6 2007 11:00 a.m. - Noon

Location: ACES

2.302

Talk Title: Analyzing Properties of Systems

Talk Abstr

act:
As the complexity of and the dependence on engineered systems
ri

ses correctness becomes ever more important. Verification
aims to prov

e or to disprove that a system''s implementation
meets its specification

. A specification asserts a set of
properties that should hold on all e

xecutions of the system.
Two areas of research are fundamental to verifi

cation:
invariant generation and decision procedures. In this talk I
describe progress in both.

I first present a strategy for letting p

roperties guide an
invariant generation procedure a form of static anal

ysis. I
then exhibit two instances of the strategy. The first augments<

br>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 ho

w to make it
property-directed.

Arrays are ubiquitous data struct

ures in software and in
hardware specifications. I present a decision p

rocedure for a
fragment of a theory of arrays that allows some quantific

ation.
Besides being expressive this fragment is interesting because
it lies on the edge of decidability: natural and simple
extensions prod

uce undecidable fragments.

Finally I briefly discuss my work with Z

ohar Manna on
developing a new undergraduate course at Stanford. Our co

urse
and accompanying forthcoming text both entitled The Calculus
of
Computation cover first-order logic; decision procedures;
and softwa

re specification verification and analysis.