There is a sign-up schedule for this event:L
ht

tp://www.cs.utexas.edu/department/webevent/utcs/events/cgi/list_events.cgi<

br>
Type of Talk: UTCS Colloquium

Speaker Name/Affiliation: Jos

e Meseguer/Univ. of Illinois at Urbana-Champaign

Date/Time: Friday
November 2 2007 11:00a.m.

Location: ACES 6.304

Host:

Jayadev Misra

Talk Title: The Temporal Logic of Rewriting

T

alk Abstract:
This talk presents the temporal logic of rewriting TLR*.

Syntactically TLR* is a very simple extension of CTL*
which just a

dds action atoms in the form of spatial
action patterns to CTL*. Sem

antically and pragmatically
however when used together with rewriting

logic as a
%60%60tandem'''' of system specification and property specif

ication
logics it has substantially more expressive power than purely

state-based logics like CTL* or purely action-based logics
like A-C

TL*. Furthermore it avoids the system/property
mismatch problem expe

rienced in state-based or action-based
logics which makes many useful

properties inexpressible in
those frameworks without unnatural changes

to a system''s
specification.

The advantages in expresiveness of
TLR* are gained without
losing the ability to use existing tools and al

gorithms to model
check its properties: a faithful translation of mode

ls and
formulas is given that allows verifying TLR* properties with
C

TL* model checkers. Simulations and bisimulations reflecting
and/or pr

eserving useful classes of TLR* properties are also
studied. Finally a

strategy language for rewriting is used as a
way to verify (resp. falsi

fy) guarantee (resp. safety) formulas
in TLR* for infinite-state system

s and more generally to verify
strategy formulas

Speaker Bio:

Dr. Jose Meseguer received a Ph.D. in Mathematics from the
Universit

y of Zaragoza Spain. He is Professor of Computer
Science at the Unive

rsity of Illinois at Urbana-Champaign (UIUC).
Prior to moving to UIUC

he was a Principal Scientist as the Stanford
Reserch Institute (SRI) a

fter having held postdoctoral positions
at the University of California
at Berkeley and IBM Research.
He was also an Initiator Member of Stan

ford University''s Center
for the Study of Language and Information (CS

LI).

Dr. Meseguer has made fundamental contributions in the frontier

between executable formal specification and verification
declarati

ve programming languages programming methodology
concurrency and sec

urity. His work in all these areas comprising
over 200 publications

is highly cited. The Maude language is one
of the most advanced and ef

ficient executable formal specification
languages. It supports a wide r

ange of formal analyses including
symbolic simulation search model c

hecking and theorem proving.
It is also an advanced declarative concu

rrent language with
sophisticated object-oriented features and powerful
module
composition and reflective metaprogramming capabilities. He <

br>his collaborators and other researchers have used Maude and
its too

l environment to build sophisticated systems and tools
and to specify a

nd analyze many systems including criptographic
protocols active netwo

rk protocols models of cell biology
executable formal semantics of pr

ogramming languages formal
analyzers for conventional code theorem pr

overs and tools for
interoperating different formal systems. He has g

iven numerous
invited lectures at international scientific meetings and
has taught
advanced courses on his research at leading American Briti

sh
German Spanish Italian and Japanese universities and research centers. He has also served in numerous program committees of
intern

ational scientific conferences and as editor of various books.