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


Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4001345