{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:10:11Z","timestamp":1763467811918},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,10,18]],"date-time":"2007-10-18T00:00:00Z","timestamp":1192665600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2007,10,30]]},"DOI":"10.1007\/s10703-007-0041-6","type":"journal-article","created":{"date-parts":[[2007,10,17]],"date-time":"2007-10-17T11:15:19Z","timestamp":1192619719000},"page":"281-305","source":"Crossref","is-referenced-by-count":20,"title":["Memory model sensitive bytecode verification"],"prefix":"10.1007","volume":"31","author":[{"given":"Thuan Quang","family":"Huynh","sequence":"first","affiliation":[]},{"given":"Abhik","family":"Roychoudhury","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,10,18]]},"reference":[{"key":"41_CR1","unstructured":"Java Specification Request (JSR) 133 (2004) Java memory model and thread specification revision"},{"key":"41_CR2","unstructured":"Abrams B. http:\/\/blogs.msdn.com\/brada\/archive\/2004\/05\/12\/130935.aspx"},{"key":"41_CR3","unstructured":"Brumme C. Weblog: memory model. http:\/\/blogs.msdn.com\/cbrumme\/archive\/2003\/05\/17\/51445.aspx"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Burckhardt S, Alur R, Martin M (2006) Bounded model checking of concurrent data types on relaxed memory models: a case study. In: International conference on computer aided verification (CAV)","DOI":"10.1007\/11817963_45"},{"key":"41_CR5","doi-asserted-by":"crossref","unstructured":"Burckhardt S, Alur R, Martin M (2007). Checkfence: checking consistency of concurrent data types on relaxed memory models. In: ACM conference on programming language design and implementation (PLDI)","DOI":"10.1145\/1250734.1250737"},{"key":"41_CR6","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge"},{"key":"41_CR7","volume-title":"Reasoning about parallel architectures","author":"WW Collier","year":"1992","unstructured":"Collier WW (1992) Reasoning about parallel architectures. Prentice Hall, New York. Details available from http:\/\/www.mpdiag.com\/archtest.html"},{"key":"41_CR8","volume-title":"Formal specification of abstract memory models. Symposium on research on integrated systems","author":"DL Dill","year":"1993","unstructured":"Dill DL, Park S, Nowatzyk A (1993) Formal specification of abstract memory models. Symposium on research on integrated systems. MIT Press, Cambridge"},{"issue":"2\u20133","key":"41_CR9","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1023\/B:FORM.0000040028.49845.67","volume":"25","author":"MB Dwyer","year":"2004","unstructured":"Dwyer MB, Hatcliff JR Prasad VR (2004) Exploiting object escape and locking information in partial order reduction for concurrent object-oriented programs. Form Methods Syst Des 25(2\u20133):199\u2013240","journal-title":"Form Methods Syst Des"},{"key":"41_CR10","unstructured":"Bacon D et al. The \u201cDouble-checked locking is broken\u201d declaration. http:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/DoubleCheckedLocking.html"},{"key":"41_CR11","doi-asserted-by":"crossref","first-page":"399","DOI":"10.4153\/CJM-1956-045-5","volume":"8","author":"LR Ford","year":"1956","unstructured":"Ford LR, Fulkerson DR (1956) Maximum flow through a network. Can J Math 8:399\u2013404","journal-title":"Can J Math"},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"Gopalakrishnan G, Yang Y, Lindstrom G (2004) QB or not QB: an efficient execution verification tool for memory orderings. In: International Conference on Computer Aided Verification (CAV)","DOI":"10.1007\/978-3-540-27813-9_31"},{"key":"41_CR13","doi-asserted-by":"crossref","unstructured":"Huynh TQ, Roychoudhury A (2006) A memory model sensitive checker for C#. In: Formal methods symposium (FM). http:\/\/www.comp.nus.edu.sg\/~abhik\/pdf\/fm06.pdf","DOI":"10.1007\/11813040_32"},{"key":"41_CR14","unstructured":"JGF (2001) The Java grande Forum Multi-threaded Benchmarks. http:\/\/www.epcc.ed.ac.uk\/computing\/research_activities\/java_grande\/threads.html"},{"key":"41_CR15","unstructured":"JPF (2005) The Java path finder model checking tool. http:\/\/javapathfinder.sourceforge.net\/"},{"issue":"9","key":"41_CR16","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport L (1979) How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans Comput 28(9):690\u2013691","journal-title":"IEEE Trans Comput"},{"key":"41_CR17","unstructured":"Lea D The JSR-133 cookbook for compiler writers. http:\/\/gee.cs.oswego.edu\/dl\/jmm\/cookbook.html"},{"key":"41_CR18","unstructured":"Manson J, Pugh W (2002) The java memory model simulator. In: Workshop on formal techniques for Java-like programs, in association with ECOOP"},{"key":"41_CR19","doi-asserted-by":"crossref","unstructured":"Manson J, Pugh W, Adve S (2005) The Java memory model. In: ACM symposium on principles of programming languages (POPL)","DOI":"10.1145\/1040305.1040336"},{"key":"41_CR20","unstructured":"Microsoft (2005) Standard ECMA-334 C# specification. http:\/\/www.ecma-international.org\/publications\/files\/ECMA-ST\/Ecma-334.pdf 1"},{"key":"41_CR21","unstructured":"Microsoft (2005) Standard ECMA-335 common language infrastructure (CLI). http:\/\/www.ecma-international.org\/publications\/standards\/Ecma-335.htm"},{"key":"41_CR22","unstructured":"Morrison V. Dotnet discussion: the DOTNET memory model. http:\/\/discuss.develop.com\/archives\/wa.exe?A2=ind0203B&L=DOTNET&P=R375"},{"key":"41_CR23","doi-asserted-by":"crossref","unstructured":"Nalumusu R et al (1998) The \u2018test model checking\u2019 approach to the verification of memory models of multiprocessors. In International conference on computer aided verification (CAV)","DOI":"10.1007\/BFb0028767"},{"key":"41_CR24","unstructured":"Nipkow T et al (2003) Special issue on Java bytecode verification. J Autom Reas 30(34)"},{"issue":"2","key":"41_CR25","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1109\/12.752664","volume":"48","author":"S Park","year":"1999","unstructured":"Park S, Dill DL (1999) An executable specification and verifier for relaxed memory order. IEEE Trans Comput 48(2):227\u2013235","journal-title":"IEEE Trans Comput"},{"key":"41_CR26","unstructured":"Pugh W Test for sequential consistency of volatiles. http:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/ReadAfterWrite.java"},{"key":"41_CR27","volume-title":"Algorithms for mutual exclusion","author":"M Raynal","year":"1986","unstructured":"Raynal M (1986) Algorithms for mutual exclusion. MIT Press, Cambridge"},{"key":"41_CR28","doi-asserted-by":"crossref","unstructured":"Roychoudhury A, Mitra T (2002) Specifying multithreaded Java semantics for program verification. In ACM international conference on software engineering (ICSE)","DOI":"10.1145\/581396.581399"},{"key":"41_CR29","unstructured":"Schmidt D, Harrison T (1996) Double-checked locking: an optimization pattern for efficiently initializing and accessing thread-safe objects. In: 3rd annual pattern languages of program design conference"},{"key":"41_CR30","series-title":"Lecture notes in computer science","volume-title":"Abstract state machines workshop","author":"RF Stark","year":"2004","unstructured":"Stark RF, Borger E (2004) An ASM specification of C# threads and the NET memory model. In: Abstract state machines workshop. Lecture notes in computer science, vol 3065. Springer, Berlin"},{"key":"41_CR31","doi-asserted-by":"crossref","unstructured":"Yang Y, Gopalakrishnan G, Lindstrom G (2004) Memory model sensitive data race analysis. In International conference on formal engineering methods (ICFEM)","DOI":"10.1007\/978-3-540-30482-1_11"},{"key":"41_CR32","doi-asserted-by":"crossref","unstructured":"Yang Y, Gopalakrishnan G, Lindstrom G, Slind K (2003) Analyzing the Intel Itanium memory ordering rules using logic programming and SAT. In: Correct hardware design and verification methods CHARME","DOI":"10.1007\/978-3-540-39724-3_9"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-007-0041-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-007-0041-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-007-0041-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:01:02Z","timestamp":1559239262000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-007-0041-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,18]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,10,30]]}},"alternative-id":["41"],"URL":"https:\/\/doi.org\/10.1007\/s10703-007-0041-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10,18]]}}}