Hello,
Please view the slides in the order,
   spr1, spr2, spr2a, spr2b, spr3, etc.

I will link them more nicely Real Soon Now.

Thanks,
Dave

P.S.  Here is the abstract to this talk:


From Trace Semantics to Modal Transition Systems: Theory and Applications

David Schmidt
Kansas State University

A software system's semantics can be defined as the set of its
execution traces.  But such a set is usually infinite, so a finite
state-transition-system representation is used instead.
Unfortunately, the transition-system representation loses precision,
so validation or refutation of a property of the transition system
does not ensure validation or refutation of the property for the
trace set. 
     To understand and improve the situation, we study trace-set
semantics and a linear-time logic for stating their properties. 
We expose the imprecisions (and even unsoundness) in state-transition
representations of trace sets, and following Cousot and Cousot,
we introduce a branching-time logic that is a sound abstract interpretation
of the linear-time logic.  To improve precision, we progress
from a state-transition formulation to a modal-transition-system
framework; we justify the correctness of modal-transition systems
by means of a binary refinement relation, and we apply the framework
and its logic to examples from software validation,
(pointer) shape analysis, and system specification.