BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verifying Object-Invariants in Spec# - Wolfram Schulte  (Microsoft
  Research Redmond)
DTSTART:20070209T140000Z
DTEND:20070209T150000Z
UID:TALK6623@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:Spec# is an experimental extension to C# that adds design-by-c
 ontract features. Contracts include method preconditions\, postconditions\
 , object invariants and history invariants. Contracts capture programmer i
 ntentions about how methods and data are to be used. The Spec# program ver
 ifier generates logical verification conditions from a Spec# program. Inte
 rnally\, it uses an automatic theorem prover that analyzes the verificatio
 n conditions to prove the correctness of the program\nor find errors in it
 . In this lecture I will present Spec# and focus on how to verify invarian
 ts in the presence of callbacks\, various forms of aliasing\, and inherita
 nce.\n\n\n\nRemark: Incorporates results from Rustan Leino\, Mike Barnett\
 , Manuel Fähndrich\, Herman Venter\, Rob DeLine (all MSR)\, Peter Müller
  and Adam Darvas (ETH)\, Bart Jacobs (KU Leuven)\, Bor-Yuh Evan Chang (Ber
 kley)\, and Angelika Wallenburg (Chalmers)
LOCATION:FW11
END:VEVENT
END:VCALENDAR