BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A unified model of class invariant verification frameworks - Sophi
 a Drossopoulou (Imperial College)
DTSTART:20070706T130000Z
DTEND:20070706T140000Z
UID:TALK7295@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:Verification of object oriented programs is usually based on\n
 class invariants\,  which express persistent properties of objects of that
 \nclass. Class invariants need  to be treated with some care\,\nmainly bec
 ause of multi-object invariants\, call-backs\,\nand their dependence on (s
 ub)-classes.\n\nSeveral verification frameworks have been suggested\, whic
 h determine at\nwhich point in a program which invariants of which object 
 are expected to\nhold\,  and which invariants of which object have to be p
 roven.\n\nThese frameworks are complex and differ in restrictions on progr
 ams\n(e.g.\, which fields can be updated)\, restrictions on invariants\n(w
 hat may an invariant refer to)\, use of advanced type systems\n(such as ow
 nership and effects)\, meaning of invariants (in which\nexecution states i
 nvariants hold)\, proof obligations (when should\nan invariant be proven).
 \n\nAs a result\, it is difficult to understand whether/why the\nframework
 s are sound\, whether/why the frameworks are modular\,\nand to compare exp
 ressiveness of the frameworks.\n\nIn this work we develop a unified model 
 to describe such frameworks\,\nand distil  seven components\, which serve 
 to characterize them. We identify\nconditions on these components under wh
 ich the framework is sound. We\ncharacterize what it means for a framework
  to be modular. We then\nspecialize the seven components  and obtain six k
 nown frameworks from the\nliterature\, and we discuss their  soundness and
  modularity. Finally\, we\ncompare expressiveness of these frameworks.\n\n
 This is joint work with Adrian Francalanza (Imperial College)\nand Peter M
 ueller (ETH Zurich and Microsoft Research).
LOCATION:FW11
END:VEVENT
END:VCALENDAR