University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > A unified model of class invariant verification frameworks

A unified model of class invariant verification frameworks

Add to your list(s) Download to your calendar using vCal

  • UserSophia Drossopoulou (Imperial College)
  • ClockFriday 06 July 2007, 14:00-15:00
  • HouseFW11.

If you have a question about this talk, please contact Matthew Parkinson.

Verification of object oriented programs is usually based on class invariants, which express persistent properties of objects of that class. Class invariants need to be treated with some care, mainly because of multi-object invariants, call-backs, and their dependence on (sub)-classes.

Several verification frameworks have been suggested, which determine at which point in a program which invariants of which object are expected to hold, and which invariants of which object have to be proven.

These frameworks are complex and differ in restrictions on programs (e.g., which fields can be updated), restrictions on invariants (what may an invariant refer to), use of advanced type systems (such as ownership and effects), meaning of invariants (in which execution states invariants hold), proof obligations (when should an invariant be proven).

As a result, it is difficult to understand whether/why the frameworks are sound, whether/why the frameworks are modular, and to compare expressiveness of the frameworks.

In this work we develop a unified model to describe such frameworks, and distil seven components, which serve to characterize them. We identify conditions on these components under which the framework is sound. We characterize what it means for a framework to be modular. We then specialize the seven components and obtain six known frameworks from the literature, and we discuss their soundness and modularity. Finally, we compare expressiveness of these frameworks.

This is joint work with Adrian Francalanza (Imperial College) and Peter Mueller (ETH Zurich and Microsoft Research).

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity