Campus Event Calendar
Event Entry
What and Who
AVACS Virtual Seminar"Limiting State Explosion"
Prof. E. Allan Emerson
University of
Texas
Virtual Seminar
AG 1, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 22 June 2007
16:30
45 Minutes
E1 4
024
Saarbrücken
Abstract
Model checking is an algorithmic method for verifying whether a given
finite state concurrent system meets a correctness specification
formulated in temporal logic, a formalism for describing change over
time. Over the past quarter century, model checking has been
demonstrated to provide the means for verifying many large systems
including industrial strength systems in a routine fashion. Model
checking works by performing a systematic search of the global system
state graph to detect patterns witnessing the truth or falsity of
temporal logic formulae. Model checking can be performed efficiently in
terms of the size of the system state graph. The fundamental limitation
to the more widespread use of model checking is the state explosion
problem, reflecting the exponential (or worse) growth of the size of the
state graph in the size of the program or design text.
We describe methods for limiting state explosion. A key theme is to exploit
regularity of system organization. For instance, systems comprised of
many homogeneous subcomponents typically posses a great deal of symmetry
that can be factored out to yield an equivalent but significantly
smaller state graph. A related task that is tractable in many situations
is parameterized model checking, where the goal is to ensure correctness
for each of the infinitely many systems of size greater than one. While
the above are oriented towards control aspects of systems, it is also
possible to reason about data. In particular, we discuss techniques for
automated reasoning about parameterized date structures, such as
arbitrarily large linked lists.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 06/21/2007 14:23
Roxane Wetzel, 06/20/2007 14:10
Roxane Wetzel, 06/15/2007 08:55
Roxane Wetzel, 06/14/2007 16:23 -- Created document.
Roxane Wetzel, 06/20/2007 14:10
Roxane Wetzel, 06/15/2007 08:55
Roxane Wetzel, 06/14/2007 16:23 -- Created document.