BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Discovery of Invariants through Automated Theory Formation - Teres
 a Rodriguez - Heriot-Watt University
DTSTART:20111025T120000Z
DTEND:20111025T130000Z
UID:TALK33702@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:Refinement is a powerful mechanism for mastering the complexit
 ies that arise when formally modelling systems. Refinement also brings wit
 h it additional proof obligations -- requiring a developer to discover pro
 perties relating to their design decisions. With the goal of reducing this
  burden\, we have investigated how a general purpose theory formation tool
 \, HR\, can be used to automate the discovery of such properties within th
 e context of Event-B. In this talk I am going to present a heuristic appro
 ach to the automatic discovery of invariants. The set of heuristics develo
 ped provides systematic guidance in tailoring HR for a given Event-B devel
 opment. These heuristics are based upon proof-failure analysis\, and have 
 given rise to some promising results
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR