{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T21:10:05Z","timestamp":1740258605112,"version":"3.37.3"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2010,7,1]],"date-time":"2010-07-01T00:00:00Z","timestamp":1277942400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2010,7]]},"DOI":"10.1007\/s11390-010-9369-2","type":"journal-article","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T22:35:33Z","timestamp":1278887733000},"page":"841-852","source":"Crossref","is-referenced-by-count":1,"title":["Formal Reasoning About Lazy-STM Programs"],"prefix":"10.1007","volume":"25","author":[{"given":"Yong","family":"Li","sequence":"first","affiliation":[]},{"given":"Yu","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Yi-Yun","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Ming","family":"Fu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,7,11]]},"reference":[{"key":"9369_CR1","doi-asserted-by":"crossref","unstructured":"Herlihy M, Moss J E B. Transactional memory: Architectural support for lock-free data structures. In Proc. the 20th Annual International Symposium on Computer Architecture (ISCA1993), San Diego, US, May 1993, pp.289-300.","DOI":"10.1145\/165123.165164"},{"key":"9369_CR2","doi-asserted-by":"crossref","unstructured":"Hammond L, Wong V, Chen M et al. Transactional memory coherence and consistency. In Proc. the 31st Annual International Symposium on Computer Architecture (ISCA2004), M\u00fcnchen, Germany, Jun. 19-23, 2004, p.102.","DOI":"10.1109\/ISCA.2004.1310767"},{"key":"9369_CR3","doi-asserted-by":"crossref","unstructured":"Ananian C S, Asanovic K, Kuszmaul B C et al. Unbounded transactional memory. In Proc. the 11th International Symposium on High-Performance Computer Architecture (HPCA2005), San Francisco, US, Feb. 12-16, 2005, pp.316-327.","DOI":"10.1109\/HPCA.2005.41"},{"key":"9369_CR4","unstructured":"Moore K E, Grossman D. Log-based transactional memory. In Proc. The Twelfth International Symposium on High-Performance Computer Architecture, Austin, USA, Feb. 11-15, 2006, pp.254-265."},{"key":"9369_CR5","doi-asserted-by":"crossref","unstructured":"Shavit N, Touitou D. Software transactional memory. In Proc. the 14th Annual ACM Symposium on Principles of Distributed Computing (PODC 1995), Ottawa, Canada, Aug. 20-23, 1995, pp.204-213.","DOI":"10.1145\/224964.224987"},{"key":"9369_CR6","doi-asserted-by":"crossref","unstructured":"Harris T, Fraser K. Language support for lightweight transactions. In Proc. the 18th Annual ACM SIGPLAN Conference on Object-Oriented Programing, Systems, Languages, and Applications (OOPSLA2003), Anaheim, USA, Oct. 26-30, 2003, pp.388-402.","DOI":"10.1145\/949338.949340"},{"key":"9369_CR7","doi-asserted-by":"crossref","unstructured":"Saha B, Adl-Tabatabai A R, Hudson R L, Minh C C, Hertzberg B.McRT-STM: A high performance software transactional memory system for a multi-core runtime. In Proc. the Eleventh ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2006), New York, USA, Mar. 29-31, 2006, pp.187-197.","DOI":"10.1145\/1122971.1123001"},{"key":"9369_CR8","doi-asserted-by":"crossref","unstructured":"Herlihy M, Luchangco V, Moir M, Scherer W N III. Software transactional memory for dynamic-sized data structures. In Proc. the 22nd Annual Symposium on Principles of Distributed Computing (PODC2003), Boston, USA, July 13-16, 2003, pp.92-101.","DOI":"10.1145\/872035.872048"},{"key":"9369_CR9","doi-asserted-by":"crossref","unstructured":"Dice D, Shalev O, Shavit N. Transactional locking II. In Proc. International Symposium on Distributed Computing, Stockholm, Sweden, Sept. 18-20, 2006, pp.194-208.","DOI":"10.1007\/11864219_14"},{"key":"9369_CR10","doi-asserted-by":"crossref","unstructured":"Felber P, Fetzer C, Riegel T. Dynamic performance tuning of word-based software transactional memory. In Proc. the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2008), Salt Lake City, USA, Feb. 20-23, 2008, pp.237-246.","DOI":"10.1145\/1345206.1345241"},{"key":"9369_CR11","doi-asserted-by":"crossref","unstructured":"Kumar S, Chu M, Hughes C J, Kundu P, Nguyen A. Hybrid transactional memory. In Proc. the 11th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2006), New York, USA, Mar. 29-31, 2006, pp.209-220.","DOI":"10.1145\/1122971.1123003"},{"key":"9369_CR12","unstructured":"Liblit B. An operational semantics for LogTM. Technical Report 1571, University of Wisconsin-Madison, August 2006."},{"issue":"2","key":"9369_CR13","first-page":"17","volume":"5","author":"M Martin","year":"2006","unstructured":"Martin M, Blundell C, Lewis E. Subtleties of transactional memory atomicity semantics. IEEE Computer Architecture Letters, 2006, 5(2): 17.","journal-title":"IEEE Computer Architecture Letters"},{"key":"9369_CR14","doi-asserted-by":"crossref","unstructured":"Moore K F, Grossman D. High-level small-step operational semantics for transactions. In Proc. the 13th ACM SIGPLAN Symposium on Principles and Practices of Parallel Programming (PPoPP 2008), Salt Lake City, USA, Feb. 20-22, 2008, pp.51-62.","DOI":"10.1145\/1328438.1328448"},{"issue":"1","key":"9369_CR15","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s11390-009-9204-9","volume":"24","author":"L Li","year":"2009","unstructured":"Li L, Zhang Y, Chen Y, Li Y. Certifying concurrent programs using transactional memory. Journal of Computer Science and Technology, Jan. 2009, 24(1): 110-121.","journal-title":"Journal of Computer Science and Technology"},{"issue":"1\u20133","key":"9369_CR16","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn P W. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 2007, 375(1-3): 271-307.","journal-title":"Theor. Comput. Sci."},{"key":"9369_CR17","doi-asserted-by":"crossref","unstructured":"Bornat R, Calcagno C, O\u2019Hearn P, Parkinson M. Permission accounting in separation logic. In Proc. the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2005), Long Beach, USA, Jan. 12-14, 2005, pp.259-270.","DOI":"10.1145\/1047659.1040327"},{"key":"9369_CR18","unstructured":"The Coq proof assistant reference manual. Coq release v8.1, Coq Development Team, October 2006."},{"key":"9369_CR19","doi-asserted-by":"crossref","unstructured":"Yu D, Shao Z. Verification of safety properties for concurrent assembly code. In Proc. the 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP 2004), Snow Bird, USA, Sept. 19-21, 2004, pp.175-188.","DOI":"10.1145\/1016848.1016875"},{"key":"9369_CR20","doi-asserted-by":"crossref","unstructured":"Feng X, Shao Z. Modular verification of concurrent assembly code with dynamic thread creation and termination. In Proc. the 2005 ACM SIGPLAN International Conference on Functional Programming (ICFP 2005), Tallinn, Estonia, Sept. 26-28, 2005, pp.254-267.","DOI":"10.1145\/1086365.1086399"},{"key":"9369_CR21","doi-asserted-by":"crossref","unstructured":"Li Y, Zhang Y, Chen Y, Fu M. On the verification of strong atomicity of programs using STM. In Proc. the 3rd IEEE Int. Conf. Secure Software Integration and Reliability Improvement (SSIRI 2009), Shanghai, China, July 8-10, 2009, pp.123-131.","DOI":"10.1109\/SSIRI.2009.8"},{"key":"9369_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds J C. Separation logic: A logic for shared mutable data structures. In Proc, the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, July 22-25, 2002, pp.55-74.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"9369_CR23","doi-asserted-by":"crossref","unstructured":"Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular verification of assembly code with stack-based control abstractions. In Proc. the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2006), Ottawa, Canada, Jun. 10-16, 2006, pp.401-414.","DOI":"10.1145\/1133981.1134028"},{"issue":"1","key":"9369_CR24","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1994","unstructured":"Wright A K, Felleisen M. A syntactic approach to type soundness. Information and Computation, 1994, 115(1): 38-94.","journal-title":"Information and Computation"},{"key":"9369_CR25","unstructured":"Li Y. Coq implementation for formal reasoning about concurrent programs using a lazy-STM system. http:\/\/ssg.ustcsz.edu.cn\/content\/formal-reasoning-about-lazy-stm-programs ."},{"issue":"4","key":"9369_CR26","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones C B. Tentative steps toward a development method for interfering programs. Transactions on Programming Languages and Systems., 1983, 5(4): 596-619.","journal-title":"Transactions on Programming Languages and Systems."},{"key":"9369_CR27","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/j.entcs.2005.11.060","volume":"155","author":"S Brookes","year":"2006","unstructured":"Brookes S. A grainless semantics for parallel programs with shared mutable data. Electron. Notes Theor. Comput. Sci., 2006, 155: 277-307.","journal-title":"Electron. Notes Theor. Comput. Sci."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-010-9369-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-010-9369-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-010-9369-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T20:30:56Z","timestamp":1740256256000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-010-9369-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,7]]}},"alternative-id":["9369"],"URL":"https:\/\/doi.org\/10.1007\/s11390-010-9369-2","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"type":"print","value":"1000-9000"},{"type":"electronic","value":"1860-4749"}],"subject":[],"published":{"date-parts":[[2010,7]]}}}