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:Computer Laboratory Automated Reasoning Group Lunc
 hes
SUMMARY:Discovery of Invariants through Automated Theory F
 ormation - Teresa Rodriguez - Heriot-Watt Universi
 ty
DTSTART;TZID=Europe/London:20111025T130000
DTEND;TZID=Europe/London:20111025T140000
UID:TALK33702AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/33702
DESCRIPTION:Refinement is a powerful mechanism for mastering t
 he complexities that arise when formally modelling
  systems. Refinement also brings with it additiona
 l proof obligations -- requiring a developer to di
 scover properties relating to their design decisio
 ns. With the goal of reducing this burden\, we hav
 e investigated how a general purpose theory format
 ion tool\, HR\, can be used to automate the discov
 ery of such properties within the context of Event
 -B. In this talk I am going to present a heuristic
  approach to the automatic discovery of invariants
 . The set of heuristics developed provides systema
 tic guidance in tailoring HR for a given Event-B d
 evelopment. These heuristics are based upon proof-
 failure analysis\, and have given rise to some pro
 mising results
LOCATION:Computer Laboratory\, William Gates Building\, Roo
 m SS03
CONTACT:William Denman
END:VEVENT
END:VCALENDAR