@techreport{TD:100682,
	att_abstract={{Mobility is a network capability with many forms and many uses.
Because it is difficult to implement at Internet scale, there is a
large and confusing landscape of mobility proposals which cannot easily
be compared or composed.
This paper presents formal models of two distinct patterns for
implementing mobility, explaining their generality and applicability.
We also employ formal verification to show that different instances of
the patterns, used for different purposes in a network architecture,
compose without alteration or interference.
This result applies to all real implementations that are refinements
of the patterns.
}},
	att_authors={pz2728},
	att_categories={},
	att_copyright={{Springer-Verlag}},
	att_copyright_notice={{The definitive version was published in  2013. {{, Volume LNCS 8164}}{{, 2014-01-01}}
}},
	att_donotupload={},
	att_private={false},
	att_projects={},
	att_tags={},
	att_techdoc={true},
	att_techdoc_key={TD:100682},
	att_url={http://web1.research.att.com:81/techdocs_downloads/TD:100682_DS1_2013-02-25T22:08:38.594Z.pdf},
	author={Pamela Zave and Jennifer Rexford},
	institution={{Fifth Working Conference on Verified Software:  Theories, Tools, and Experiments}},
	month={January},
	title={{Compositional Network Mobility}},
	year=2014,
}