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:Verifying Object-Invariants in Spec# - Wolfram Sch
 ulte  (Microsoft Research Redmond)
DTSTART;TZID=Europe/London:20070209T140000
DTEND;TZID=Europe/London:20070209T150000
UID:TALK6623AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/6623
DESCRIPTION:Spec# is an experimental extension to C# that adds
  design-by-contract features. Contracts include me
 thod preconditions\, postconditions\, object invar
 iants and history invariants. Contracts capture pr
 ogrammer intentions about how methods and data are
  to be used. The Spec# program verifier generates 
 logical verification conditions from a Spec# progr
 am. Internally\, it uses an automatic theorem prov
 er that analyzes the verification conditions to pr
 ove the correctness of the program\nor find errors
  in it. In this lecture I will present Spec# and f
 ocus on how to verify invariants in the presence o
 f callbacks\, various forms of aliasing\, and inhe
 ritance.\n\n\n\nRemark: Incorporates results from 
 Rustan Leino\, Mike Barnett\, Manuel Fähndrich\, H
 erman Venter\, Rob DeLine (all MSR)\, Peter Müller
  and Adam Darvas (ETH)\, Bart Jacobs (KU Leuven)\,
  Bor-Yuh Evan Chang (Berkley)\, and Angelika Walle
 nburg (Chalmers)
LOCATION:FW11
CONTACT:Matthew Parkinson
END:VEVENT
END:VCALENDAR