@techreport{TD:100968,
	att_abstract={{Because potential users have to choose a formal method before they
can start using one, evidence
suggests that research on assessing and explaining
the applicability of specific formal methods
might be as effective in encouraging their use as
work on the methods themselves.
This comparison of Alloy and Spin is based on a demanding project
that exploited the full capabilities of both languages and tools.
The conclusions contradict conventional wisdom and expectations on
several points.
Although the scope of the comparison is narrow with respect to
the systems being modeled, it is broad with respect to the range of
activities and goals involved in using formal methods.}},
	att_authors={pz2728},
	att_categories={C_NSS.16, C_NSS.4},
	att_copyright={{Springer}},
	att_copyright_notice={{The definitive version was published in  2014. {{, Volume 27}}{{, 2015-01-01}}
}},
	att_donotupload={},
	att_private={false},
	att_projects={},
	att_tags={software verification,  software analysis,  DHT,  Chord},
	att_techdoc={true},
	att_techdoc_key={TD:100968},
	att_url={http://web1.research.att.com:81/techdocs_downloads/TD:100968_DS1_2012-08-16T16:17:39.391Z.pdf},
	author={Pamela Zave},
	institution={{Formal Aspects of Computing}},
	month={January},
	title={{A Practical Comparison of Alloy and Spin}},
	year=2015,
}