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.},


Sections de Publications

Contact | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 876291