BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification Based on Algebra and Automated Deduction - Georg Stru
 th\, Sheffield University
DTSTART:20080502T130000Z
DTEND:20080502T140000Z
UID:TALK11870@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:The formal formal analysis and verification of computing\nsyst
 ems has so far been dominated by model checkers and other decision\nproced
 ures which are fully automated\, but limited in expressive power\,\nand by
  interactive theorem provers which are quite expressive\, but\nlimited in 
 automation. Due to improved hardware and theoretical\ndevelopments\, autom
 ated deduction is currently emerging as a third way\nin which expressivity
  and computational power are differently balanced\nand which conveniently 
 complements the other approaches.\n\nI will present a new approach to form
 al verification in which\ncomputational algebras are combined with off-the
 -shelf automated\ntheorem provers for first-order equational logic. The al
 gebras\nconsidered are variants of Kleene algebras and their extensions by
 \nmodal operators. Particular strengths of these structures are\nsyntactic
  simplicity\, wide applicability\, concise elegant equational\nproofs\, ea
 sy mechanisability and strong decidability.\n\nI will sketch the axiomatis
 ation and calculus of Kleene algebras and\nmodal Kleene algebras\, discuss
  some computationally interesting\nmodels\, such as traces\, graphs\, lang
 uages and relations\, and point out\ntheir relationship to popular verific
 ation formalisms\, including\ndynamic logic\, temporal logic and Hoare log
 ic. I will also report on\nsome automation results in the areas of action 
 system refinement\,\ntermination analysis and program verification that de
 monstrate the\nbenefits and the potential of the algebraic approach.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR