{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,23]],"date-time":"2025-05-23T04:38:38Z","timestamp":1747975118413,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319174037"},{"type":"electronic","value":"9783319174044"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17404-4_9","type":"book-chapter","created":{"date-parts":[[2015,4,16]],"date-time":"2015-04-16T08:45:59Z","timestamp":1429173959000},"page":"127-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Combining Separation Logic and Projection Temporal Logic to Reason About Non-blocking Concurrency"],"prefix":"10.1007","author":[{"given":"Xiaoxiao","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,17]]},"reference":[{"key":"9_CR1","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Elsevier, Amsterdam (2009)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Ashcroft, Edward, A.: Proving assertions about parallel programs. J. Comput. Syst. Sci. 10(1), 110\u2013135 (1975)","DOI":"10.1016\/S0022-0000(75)80018-3"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI, pp. 338\u2013349. ACM Press, New York (2003)","DOI":"10.1145\/780822.781169"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BFb0055631","volume-title":"CONCUR \u201998 Concurrency Theory","author":"E Cohen","year":"1998","unstructured":"Cohen, E., Lamport, L.: Reduction in TLA. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 317\u2013331. Springer, Heidelberg (1998)"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F., et al.: Safe concurrency for aggregate objects with invariants. In: Proceedings of the 3rd IEEE Conference on Software Engineering and Formal Methods. pp. 137\u2013147. (2005)","DOI":"10.1109\/SEFM.2005.39"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/11901433_23","volume-title":"Formal Methods and Software Engineering","author":"B Jacobs","year":"2006","unstructured":"Jacobs, B., Smans, J., Piessens, F., Schulte, W.: A statically verifiable programming model for concurrent object-oriented programs. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 420\u2013439. Springer, Heidelberg (2006)"},{"issue":"2","key":"9_CR7","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.entcs.2005.04.026","volume":"137","author":"R Colvin","year":"2005","unstructured":"Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. Electron. Notes Theor. Comput. Sci. 137(2), 93\u2013110 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30232-2_7","volume-title":"Formal Techniques for Networked and Distributed Systems\u2014FORTE 2004","author":"S Doherty","year":"2004","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97\u2013114. Springer, Heidelberg (2004)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-71316-6_13","volume-title":"Programming Languages and Systems","author":"X Feng","year":"2007","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 173\u2013188. Springer, Heidelberg (2007)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: POPL, pp. 315\u2013327. ACM Press, New York (2009)","DOI":"10.1145\/1594834.1480922"},{"key":"9_CR11","unstructured":"Vafeiadis, V.: Modular Fine-Grained Concurrency Verification. Cambridge University, Cambridge (2008)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. In: Proceedings of the International Symposium Semantics of Concurrent Computation. LNCS, vol. 70, pp. 1\u201320. Springer-Verlag (1979)","DOI":"10.1007\/BFb0022460"},{"issue":"1\u20133","key":"9_CR14","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/S0747-7171(89)80070-7","volume":"8","author":"M Abadi","year":"1989","unstructured":"Abadi, M., Manna, Z.: Temporal logic programming. J. Symbolic Comput. 8(1\u20133), 277\u2013295 (1989)","journal-title":"J. Symbolic Comput."},{"issue":"3","key":"9_CR15","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"9_CR16","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0096-0551(98)00009-5","volume":"24","author":"P Rondogiannis","year":"1998","unstructured":"Rondogiannis, P., Gergatsoulis, M., Panayiotopoulos, T.: Branching-time logic programming: the language cactus and its applications. Comput. Lang. 24(3), 155\u2013178 (1998)","journal-title":"Comput. Lang."},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Moszkowski, B.C.: Executing Temporal Logic Programs. Cambridge University Press, Cambridge (1986)","DOI":"10.1007\/3-540-15670-4_6"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/11562931_27","volume-title":"Logic Programming","author":"Z Duan","year":"2005","unstructured":"Duan, Z., Yang, X., Koutny, M.: Semantics of framed temporal logic programs. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 356\u2013370. Springer, Heidelberg (2005)"},{"issue":"1","key":"9_CR19","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.jlap.2008.08.001","volume":"78","author":"X Yang","year":"2008","unstructured":"Yang, X., Duan, Z.: Operational semantics of framed tempura. J. Log. Algebraic Program. 78(1), 22\u201351 (2008)","journal-title":"J. Log. Algebraic Program."},{"issue":"1","key":"9_CR20","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/BF02944904","volume":"19","author":"Z Duan","year":"2004","unstructured":"Duan, Z., Koutny, M.: A framed temporal logic programming language. J. Comput. Sci. Technol. 19(1), 341\u2013351 (2004)","journal-title":"J. Comput. Sci. Technol."},{"key":"9_CR21","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatic 45, 43\u201378 (2008)","journal-title":"Acta Informatic"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"10","key":"9_CR23","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). and 583","journal-title":"Commun. ACM"},{"issue":"1\u20133","key":"9_CR24","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW OHearn","year":"2007","unstructured":"OHearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-34281-3_5","volume-title":"Formal Methods and Software Engineering","author":"X Yang","year":"2012","unstructured":"Yang, X., Zhang, Y., Fu, M., Feng, X.: A concurrent temporal programming model with atomic blocks. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 22\u201337. Springer, Heidelberg (2012)"},{"issue":"5","key":"9_CR26","first-page":"1069","volume":"36","author":"X Wang","year":"2008","unstructured":"Wang, X., Duan, Z.: Pointers in framing projection temporal logic programming language. J. Xidian Univ. 36(5), 1069\u20131074 (2008)","journal-title":"J. Xidian Univ."},{"issue":"5","key":"9_CR27","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1017\/S0960129510000241","volume":"20","author":"X Yang","year":"2010","unstructured":"Yang, X., Duan, Z., Ma, Q.: Axiomatic semantics of projection temporal logic programs. Math. Struct. Comput. Sci. 20(5), 865\u2013914 (2010)","journal-title":"Math. Struct. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17404-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T16:43:56Z","timestamp":1747932236000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17404-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319174037","9783319174044"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17404-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"17 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}