乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T16:02:09Z","timestamp":1732032129442},"reference-count":33,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2007,3,1]],"date-time":"2007-03-01T00:00:00Z","timestamp":1172707200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":2330,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Journal of Logic and Algebraic Programming"],"published-print":{"date-parts":[[2007,3]]},"DOI":"10.1016\/j.jlap.2006.08.007","type":"journal-article","created":{"date-parts":[[2006,9,27]],"date-time":"2006-09-27T07:39:02Z","timestamp":1159342742000},"page":"1-43","source":"Crossref","is-referenced-by-count":9,"title":["Model checking a cache coherence protocol of a Java DSM implementation"],"prefix":"10.1016","volume":"71","author":[{"given":"Jun","family":"Pang","sequence":"first","affiliation":[]},{"given":"Wan","family":"Fokkink","sequence":"additional","affiliation":[]},{"given":"Rutger","family":"Hofman","sequence":"additional","affiliation":[]},{"given":"Ronald","family":"Veldema","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.jlap.2006.08.007_bib1","article-title":"Process Algebra","volume":"vol. 18","author":"Baeten","year":"1990"},{"issue":"3","key":"10.1016\/j.jlap.2006.08.007_bib2","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/s00165-005-0070-0","article-title":"Verification of a sliding window protocol in \u03bcCRL and PVS","volume":"17","author":"Badban","year":"2005","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/j.jlap.2006.08.007_bib3","series-title":"Proc. 13th Conference on Computer Aided Verification","first-page":"250","article-title":"\u03bcCRL: a tool set for analysing algebraic specifications","volume":"vol. 2102","author":"Blom","year":"2001"},{"key":"10.1016\/j.jlap.2006.08.007_bib4","doi-asserted-by":"crossref","unstructured":"S.C.C. Blom, I. van Langevelde, B. Lisser, Compressed and distributed file formats for labeled transition systems, in: Proc. 2nd Workshop on Parallel and Distributed Model Checking, ENTCS 89(1), Elsevier, 2003, pp. 68\u201383.","DOI":"10.1016\/S1571-0661(05)80097-0"},{"key":"10.1016\/j.jlap.2006.08.007_bib5","doi-asserted-by":"crossref","unstructured":"S.C.C. Blom, S.M. Orzan, Distributed branching bisimulation reduction of state spaces, in: Proc. 2nd Workshop on Parallel and Distributed Model Checking, ENTCS 89(1), Elsevier, 2003, pp. 99\u2013113.","DOI":"10.1016\/S1571-0661(05)80099-4"},{"key":"10.1016\/j.jlap.2006.08.007_bib6","series-title":"Formal Systems Specification: The RPC-Memory Specification Case Study","volume":"vol. 1169","year":"1996"},{"key":"10.1016\/j.jlap.2006.08.007_bib7","series-title":"Model Checking","author":"Clarke","year":"2000"},{"key":"10.1016\/j.jlap.2006.08.007_bib8","series-title":"Proc. 12th Conference on Computer Aided Verification","first-page":"53","article-title":"Automatic verification of parameterized cache coherence protocols","volume":"vol. 1855","author":"Delzanno","year":"2000"},{"key":"10.1016\/j.jlap.2006.08.007_bib9","doi-asserted-by":"crossref","unstructured":"M. Dubois, J.-C. Wang, L. Barroso, K. Lee, Y.-S. Chen, Delayed consistency and its effects on the miss rate of parallel programs, in: Proc. 1991 ACM\/IEEE Conference on Supercomputing, 1991, pp. 197\u2013206.","DOI":"10.1145\/125826.125941"},{"key":"10.1016\/j.jlap.2006.08.007_bib10","first-page":"13","article-title":"An overview of CADP 2001","volume":"4","author":"Garavel","year":"2002","journal-title":"Eur. Assoc. Software Sci. Technol. Newslett."},{"key":"10.1016\/j.jlap.2006.08.007_bib11","series-title":"The Java Language Specification","author":"Gosling","year":"1996"},{"issue":"1\u20132","key":"10.1016\/j.jlap.2006.08.007_bib12","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S1567-8326(02)00038-3","article-title":"Analysis of a distributed system for lifting trucks","volume":"55","author":"Groote","year":"2003","journal-title":"J. Log. Algebr. Program."},{"key":"10.1016\/j.jlap.2006.08.007_bib13","series-title":"Proc. 1st Workshop on the Algebra of Communicating Processes","first-page":"26","article-title":"The syntax and semantics of \u03bcCRL","author":"Groote","year":"1995"},{"issue":"1\/2","key":"10.1016\/j.jlap.2006.08.007_bib14","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S1567-8326(01)00005-4","article-title":"Linearization in parallel pCRL","volume":"48","author":"Groote","year":"2001","journal-title":"J. Log. Algebr. Program."},{"key":"10.1016\/j.jlap.2006.08.007_bib15","series-title":"Handbook of Process Algebra","first-page":"1151","article-title":"Algebraic process verification","author":"Groote","year":"2001"},{"key":"10.1016\/j.jlap.2006.08.007_bib16","series-title":"Proc. 11th Conference on Computer-Aided Verification","first-page":"301","article-title":"Verifying sequential consistency on shared memory multiprocessor systems","volume":"vol. 1633","author":"Henzinger","year":"1999"},{"key":"10.1016\/j.jlap.2006.08.007_bib17","unstructured":"P. Keleher, A. Cox, S. Dwarkadas, W. Zwaenepoel, TreadMarks: distributed shared memory on standard workstations and operating systems, in: Proc. USENIX Winter 1994 Conference, 1994, pp. 115\u2013132."},{"issue":"9","key":"10.1016\/j.jlap.2006.08.007_bib18","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","article-title":"How to make a multiprocessor computer that correctly executes multiprocess program","volume":"28","author":"Lamport","year":"1979","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/j.jlap.2006.08.007_bib19","series-title":"Specification of Abstract Data Types","author":"Loeckx","year":"1996"},{"key":"10.1016\/j.jlap.2006.08.007_bib20","unstructured":"J. Maessen, Arvind, X. Shen, Improving the Java memory model using CRF, in: Proc. 2000 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, 2000, pp. 1\u201312."},{"key":"10.1016\/j.jlap.2006.08.007_bib21","doi-asserted-by":"crossref","unstructured":"J. Manson, W. Pugh, Core semantics of multithreaded Java, in: Proc. ACM 2001 Java Grande Conference, 2001 pp. 29\u201338.","DOI":"10.1145\/376656.376806"},{"issue":"3","key":"10.1016\/j.jlap.2006.08.007_bib22","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","article-title":"Efficient on-the-fly model-checking for regular alternation-free mu-calculus","volume":"46","author":"Mateescu","year":"2003","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jlap.2006.08.007_bib23","series-title":"Proc. 5th Conference on Coordination Models and Languages","first-page":"274","article-title":"Formal specification of JavaSpaces\u2122 architecture using \u03bcCRL","volume":"vol. 2315","author":"van de Pol","year":"2002"},{"issue":"9","key":"10.1016\/j.jlap.2006.08.007_bib24","doi-asserted-by":"crossref","first-page":"989","DOI":"10.1109\/71.879780","article-title":"Formal automatic verification of cache coherence in multiprocessors with relaxed memory models","volume":"11","author":"Pong","year":"2000","journal-title":"IEEE Trans. Parallel Distributed Syst."},{"key":"10.1016\/j.jlap.2006.08.007_bib25","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/BF00265555","article-title":"Fairness and related properties in transition systems \u2013 a temporal logic to deal with fairness","volume":"19","author":"Queille","year":"1983","journal-title":"Acta Inform."},{"key":"10.1016\/j.jlap.2006.08.007_bib26","doi-asserted-by":"crossref","unstructured":"A. Roychoudhury, T. Mitra, Specifying multithreaded Java semantics for program verification, in: Proc. ACM SIGSOFT Conference on Software Engineering, 2002, pp. 192\u2013201.","DOI":"10.1145\/581396.581399"},{"key":"10.1016\/j.jlap.2006.08.007_bib27","doi-asserted-by":"crossref","unstructured":"X. Shen, Arvind, L. Rodolph, Cachet: an adaptive cache coherence protocol of distributed shared memory systems, in: Proc. 13th ACM Conference on Supercomputing, 1999, pp. 135\u2013144.","DOI":"10.1145\/305138.305187"},{"key":"10.1016\/j.jlap.2006.08.007_bib28","series-title":"Proc. 11th Symposium of Formal Methods Europe","first-page":"43","article-title":"Proofs of correctness of cache-coherence protocols","volume":"vol. 2021","author":"Stoy","year":"2001"},{"key":"10.1016\/j.jlap.2006.08.007_bib29","doi-asserted-by":"crossref","unstructured":"R. Veldema, R.F.H. Hofman, R. Bhoedjang, H. Bal, Runtime-optimizations for a Java DSM, in: Proc. ACM 2001 Java Grande Conference, 2001, pp. 89\u201398.","DOI":"10.1145\/376656.376842"},{"key":"10.1016\/j.jlap.2006.08.007_bib30","doi-asserted-by":"crossref","unstructured":"R. Veldema, R.F.H. Hofman, R. Bhoedjang, C. Jacobs, H. Bal, Source-level global optimizations for fine-grain distributed shared memory systems, in: Proc. 8th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2001, pp. 83\u201392.","DOI":"10.1145\/379539.379578"},{"key":"10.1016\/j.jlap.2006.08.007_bib31","doi-asserted-by":"crossref","unstructured":"Y. Yang, G. Gopalakrishnan, G. Lindstrom, Analyzing the CRF Java memory model, in: Proc. 8th Asia-Pacific Software Engineering Conference, 2001, pp. 21\u201328.","DOI":"10.1109\/APSEC.2001.991455"},{"key":"10.1016\/j.jlap.2006.08.007_bib32","doi-asserted-by":"crossref","unstructured":"Y. Yang, G. Gopalakrishnan, G. Lindstrom, Specifying Java thread semantics using a uniform memory model, in: Proc. ACM 2002 Java Grande Conference, 2002, pp. 192\u2013201.","DOI":"10.1145\/583810.583832"},{"key":"10.1016\/j.jlap.2006.08.007_bib33","doi-asserted-by":"crossref","unstructured":"Y. Zhou, L. Iftode, K. Li, Performance evaluation of two home-based lazy release-consistency protocols for shared virtual memory systems, in: Proc. 2nd USENIX Symposium on Operating Systems Design and Implementation, 1996, pp. 75\u201388.","DOI":"10.1145\/238721.238763"}],"container-title":["The Journal of Logic and Algebraic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S156783260600049X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S156783260600049X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,21]],"date-time":"2019-04-21T06:10:44Z","timestamp":1555827044000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S156783260600049X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,3]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,3]]}},"alternative-id":["S156783260600049X"],"URL":"https:\/\/doi.org\/10.1016\/j.jlap.2006.08.007","relation":{},"ISSN":["1567-8326"],"issn-type":[{"value":"1567-8326","type":"print"}],"subject":[],"published":{"date-parts":[[2007,3]]}}}