2Brian Goetz,Tim Peierls,Joshua Bloch,et al.Java concurrency in practice[M].Addison Wesley Professional,2006.
3Holzmann G J. The spin model checker: Primer and reference manual[M].Addison-Wesley,2004.
4Holzmann G J.Trends in software verification[C].International Symposium of Formal Methods Europe,2003.
5Havehmd K, Visser W.Program model checking as a new trend [J]. International Journal on Software Tools for Technology Transfer,2002,4(1):8-20.
6Corbett J C,Dwyer M B,Hatcliff J et al.Bandera: Extracting finite-state models from java source code[C].22nd International Conference on Soilware Engineering,2000.
7David Y W Park,Ulrich Stern,Jens U Skakkebak, et al.Java model checking[C].Proceedings ASE,2000.
8Havelund K, Pressburger T.Model checking programs using Java pathfinder[J].Intemational Journal on Software Tools for Technology Transfer,2000,2(4):366-381.
9Holzmann G J.Logic verification of ANSI C code with SPIN[C]. Proc 7th Int'l SPIN Workshop Model Checking of Software, 2000.
10Samik Basu, Seott A Smolka.Model checking the Java metalocking algorithm[J].ACM Transactions on Software Engineering and Methodology,2007.
