@techreport{TD:100729,
	att_abstract={{Modeling in Alloy and analysis with the Alloy Analyzer is used to
improve our understanding of the correctness of
the Chord ring-maintenance protocol.
Correctness in this case would mean that every member of the network
is eventually reachable from every other, which is a more fundamental
notion of correctness than key or data consistency.
No published version of Chord is correct, although a version selecting
the best pieces from several papers may be correct.
The paper discusses the significance of these results, and how
lightweight modeling can contribute to protocol design.}},
	att_authors={pz2728},
	att_categories={},
	att_copyright={{}},
	att_copyright_notice={{}},
	att_donotupload={},
	att_private={false},
	att_projects={},
	att_tags={Alloy,  Spin,  distributed hash table (DHT)},
	att_techdoc={true},
	att_techdoc_key={TD:100729},
	att_url={http://web1.research.att.com:81/techdocs_downloads/TD:100729_DS1_2011-11-19T16:37:47.098Z.pdf},
	author={Pamela Zave},
	institution={{SIGCOMM Computer Communications Review}},
	month={April},
	title={{Using Lightweight Modeling to Understand Chord}},
	year=2012,
}