A unified model of class invariant verification frameworks

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

• Sophia Drossopoulou (Imperial College)
• Friday 06 July 2007, 14:00-15:00
• FW11.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW11
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.