Paper Info
Title
Relaxing Restrictions on Invariant Composition in the B Method by Ownership Control a laSpec
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.
Year
DOI
Venue
2009
10.1007/978-3-642-11447-2_1
Rigorous Methods for Software Construction and Analysis
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
1
2
Name
Order
Citations
PageRank
Sylvain Boulmé1505.69
Marie-Laure Potet219021.34