BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Verification Based on Algebra and Automated Deduct
ion - Georg Struth\, Sheffield University
DTSTART;TZID=Europe/London:20080502T140000
DTEND;TZID=Europe/London:20080502T150000
UID:TALK11870AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/11870
DESCRIPTION:The formal formal analysis and verification of com
puting\nsystems has so far been dominated by model
checkers and other decision\nprocedures which are
fully automated\, but limited in expressive power
\,\nand by interactive theorem provers which are q
uite expressive\, but\nlimited in automation. Due
to improved hardware and theoretical\ndevelopments
\, automated deduction is currently emerging as a
third way\nin which expressivity and computational
power are differently balanced\nand which conveni
ently complements the other approaches.\n\nI will
present a new approach to formal verification in w
hich\ncomputational algebras are combined with off
-the-shelf automated\ntheorem provers for first-or
der equational logic. The algebras\nconsidered are
variants of Kleene algebras and their extensions
by\nmodal operators. Particular strengths of these
structures are\nsyntactic simplicity\, wide appli
cability\, concise elegant equational\nproofs\, ea
sy mechanisability and strong decidability.\n\nI w
ill sketch the axiomatisation and calculus of Klee
ne algebras and\nmodal Kleene algebras\, discuss s
ome computationally interesting\nmodels\, such as
traces\, graphs\, languages and relations\, and po
int out\ntheir relationship to popular verificatio
n formalisms\, including\ndynamic logic\, temporal
logic and Hoare logic. I will also report on\nsom
e automation results in the areas of action system
refinement\,\ntermination analysis and program ve
rification that demonstrate the\nbenefits and the
potential of the algebraic approach.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Matthew Parkinson
END:VEVENT
END:VCALENDAR