@incollection{BP9,
title = { Relaxing Restrictions on Invariant Composition in the B method by Spec# ownership control \`a la Spec# },
author = {Boulm\'e, Sylvain and Potet, Marie-Laure},
year = {2009},
booktitle = {Rigorous Methods for Software Construction and Analysis},
publisher = {Springer Berlin / Heidelberg},
team = {DCS, PACSS},
abstract = {This paper deals with modular verification of component invariants in the B Method. On the one hand, B imposes severe architecture restrictions that ensure soundness of component compositions with a few additional proof obligations. On the other hand, in the context of the verification of object oriented programs, Spec# proposes a more expressive approach, but at the price of more complex specifications, and more numerous proof obligations. In this paper, we investigate an intermediate solution combining the advantages of both approaches.},
}
