1Goetz B, Peierls T, Bloch J, et al. Java Concurrency in Practice[M]. Addison WesleyProfessional,2006.
2Corbett J C, Dwyer M B, Hatcliff J, et al. Bandera:Extracting Finite-State Models from Java Source Code[C]//Proe of the 22nd Int' 1 Conf on Software Engineering, 2000: 439-448.
3David Y W Park, Ulrich Stem, Jens U Skakkebak, et al. Java Model Checking[C]//Proc of ASE' 00,2000.
4Havelund K, Pressburger T. Model Checking Programs Using Java Pathfinder[J].International Journal on Software Tools for Technology Transfer, 2000,2(4) : 366-381.
5Gosling J, Joy W, Steele G, et al. The Java Language Specification[M]. Third Edition. Addison Wesley, 2005.
6Clarke E M, Emerson E A, Sistla A P. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications[J].ACM Trans on Programming Languages and Systems, 1986,8(2) : 244-263.
7Holzmann G J. The Model Checker SPIN [J]. IEEE Trans on Software Engineering, 1997,23(5) : 279-94.
8Holzmann G J. Trends in Software Verifieation[C]//Proc of Int'l Symp of Formal Methods Europe, 2003:40-50.
9Havelund K, Visser W. Program Model Checking as a New Trend [J]. International Journal on Software Tools for Technology Transfer, 2002,4 (1) : 8-20.
10Pugh W. Fixing the Java Memory Model[C]//Proc of the ACM Java Grande Conf, 1999:89-98.
