{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T08:45:30Z","timestamp":1773996330255,"version":"3.50.1"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2014,1,29]],"date-time":"2014-01-29T00:00:00Z","timestamp":1390953600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2014,7]]},"DOI":"10.1007\/s10472-013-9389-z","type":"journal-article","created":{"date-parts":[[2014,1,28]],"date-time":"2014-01-28T10:19:56Z","timestamp":1390904396000},"page":"131-174","source":"Crossref","is-referenced-by-count":26,"title":["RGITL: A temporal logic framework for compositional reasoning about interleaved programs"],"prefix":"10.1007","volume":"71","author":[{"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bogdan","family":"Tofan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00f6rg","family":"Pf\u00e4hler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,1,29]]},"reference":[{"key":"9389_CR1","first-page":"1","volume-title":"Stepwise Refinement of Distributed Systems - Models, Formalisms, Correctness, vol. 430","author":"M Abadi","year":"1989","unstructured":"Abadi, M., Lamport, L.: Composing specifications. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) Stepwise Refinement of Distributed Systems - Models, Formalisms, Correctness, vol. 430, pp. 1\u201341. Springer LNCS, Berlin (1989)"},{"key":"9389_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: Conjoining Specifications. ACM Transactions on Programming Languages and Systems, pp. 507\u2013534 (1995)","DOI":"10.1145\/203095.201069"},{"key":"9389_CR3","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"SV Adve","year":"1995","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. IEEE Comput. 29, 66\u201376 (1995)","journal-title":"IEEE Comput."},{"key":"9389_CR4","doi-asserted-by":"crossref","unstructured":"Apt, K.R., de Boer, F., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 3rd edn. Springer (2009)","DOI":"10.1007\/978-1-84882-745-5"},{"issue":"2, 3","key":"9389_CR5","doi-asserted-by":"crossref","first-page":"285","DOI":"10.3233\/AIC-2010-0458","volume":"23","author":"S B\u00e4umler","year":"2010","unstructured":"B\u00e4umler, S., Balser, M., Nafz, F., Reif, W., Schellhorn, G.: Interactive verification of concurrent systems using symbolic execution. AI Commun. 23(2, 3), 285\u2013307 (2010)","journal-title":"AI Commun."},{"issue":"1","key":"9389_CR6","first-page":"91","volume":"23","author":"S B\u00e4umler","year":"2011","unstructured":"B\u00e4umler, S., Schellhorn, G., Tofan, B., Reif, W.: Proving linearizability with temporal logic. FAC J. 23(1), 91\u2013112 (2011)","journal-title":"FAC J."},{"key":"9389_CR7","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Manna, Z., Sipma, H., Uribe, T.: Deductive verification of real-time systems using STeP. Theor. Comput. Sci. 253(1) (2001)","DOI":"10.1016\/S0304-3975(00)00088-8"},{"key":"9389_CR8","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines \u2014 A Method for High-Level System Design and Analysis. Springer (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"issue":"1\u20133","key":"9389_CR9","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1\u20133), 227\u2013270 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"9389_CR10","first-page":"309","volume":"74","author":"RM Burstall","year":"1974","unstructured":"Burstall, R.M.: Program proving as hand simulation with a little induction. Inf. Process. 74, 309\u2013312 (1974)","journal-title":"Inf. Process."},{"key":"9389_CR11","unstructured":"Cau, A., Moszkowski, B.: Using PVS for Interval Temporal Logic proofs. Part 1: The syntactic and semantic encoding. Tech. rep., De Montfort University (1996)"},{"key":"9389_CR12","unstructured":"Cau, A., Moszkowski, B.: ITL \u2013 Interval Temporal Logic. Software Technology Research Laboratory. De Montfort University, UK. www.tech.dmu.ac.uk\/STRL\/ITL (2013). Accessed 1 July 2013"},{"key":"9389_CR13","doi-asserted-by":"crossref","first-page":"807","DOI":"10.1093\/logcom\/exm030","volume":"17","author":"JW Coleman","year":"2007","unstructured":"Coleman, J.W., Jones, C.B.: A structural proof of the soundness of rely\/guarantee rules. J. Log. Comput. 17, 807\u2013841 (2007)","journal-title":"J. Log. Comput."},{"key":"9389_CR14","doi-asserted-by":"crossref","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: FORTE 2004, LNCS, vol. 3235, pp. 97\u2013114 (2004)","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"9389_CR15","unstructured":"Dongol, B., Derrick, J., Hayes, I.J.: Fractional permissions and non-deterministic evaluators in interval temporal logic. ECEASST 53 (2012)"},{"key":"9389_CR16","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Proceedings of the Symposium on Applied Mathematics, vol. 19, pp. 19\u201332. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"9389_CR17","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Cook, B., Parkinson, M., Vafeiadis, V.: Proving that nonblocking algorithms don\u2019t block. In: POPL, pp. 16\u201328. ACM (2009)","DOI":"10.1145\/1594834.1480886"},{"key":"9389_CR18","unstructured":"Groves, L.: Verifying michael and scott\u2019s lock-free queue algorithm using trace reduction. In: Proceedings on CATS \u201908, pp. 133\u2013142. Australian Computer Society Inc (2008)"},{"issue":"6","key":"9389_CR19","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S1571-0661(04)80472-9","volume":"65","author":"DP Guelev","year":"2002","unstructured":"Guelev, D.P., Van Hung, D.: Prefix and projection onto state in duration calculus. Electr. Notes Theor. Comput. Sci. 65(6), 101\u2013119 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9389_CR20","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"issue":"3","key":"9389_CR21","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Prog. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"9389_CR22","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison Wesley (2003)"},{"key":"9389_CR23","unstructured":"Jacobs, B., Piessens, F.: The VeriFast Program Verifier. Technical Report CW-520. KU Leuven (2008)"},{"key":"9389_CR24","unstructured":"Jones, C.B.: Development Methods for Computer Programs Including a Notion of Interference. Ph.D. thesis, Oxford University. Available as Programming Research Group Technical Monograph 25 (1981)"},{"key":"9389_CR25","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP\u201983, pp. 321\u2013332. North-Holland (1983)"},{"key":"9389_CR26","unstructured":"King, J.C.: A Program Verifier. Ph.D. Thesis. Carnegie Mellon University (1970)"},{"key":"9389_CR27","unstructured":"KIV Download: http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/kiv (2012). Accessed 1 September 2013"},{"key":"9389_CR28","unstructured":"KIV: Presentation of a higher-order specifications of RGITL. http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/RGITL.html (2012). Accessed 1 September 2013"},{"key":"9389_CR29","unstructured":"KIV: Presentation of proofs for concurrent algorithms in RGITL. http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/lock-free.html (2013). Accessed 1 September 2013"},{"issue":"3","key":"9389_CR30","doi-asserted-by":"crossref","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). doi: 10.1145\/177492.177726","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9389_CR31","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems \u2013 Safety. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"9389_CR32","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnuelli, A.: Temporal verification diagrams. In: Hagiya, M., Mitchell, J. (eds.) International Symposium on Theoretical Aspects of Computer Software, vol. 789, pp. 726\u2013765. Springer Verlag (1994)","DOI":"10.1007\/3-540-57887-0_123"},{"key":"9389_CR33","unstructured":"Massalin, H., Pu, C.: A Lock-Free Multiprocessor OS Kernel. Tech. Rep. CUCS-005-91. Columbia University (1991)"},{"issue":"6","key":"9389_CR34","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1109\/TPDS.2004.8","volume":"15","author":"MM Michael","year":"2004","unstructured":"Michael, M.M.: Hazard pointers: safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst 15(6), 491\u2013504 (2004)","journal-title":"IEEE Trans. Parallel Distrib. Syst"},{"key":"9389_CR35","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of the 15th ACM Symposium on Principles of Distributed Computing, pp. 267\u2013275 (1996)","DOI":"10.1145\/248052.248106"},{"key":"9389_CR36","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. 7, 417\u2013426 (1981)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9389_CR37","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1023\/A:1008624904634","volume":"14","author":"JS Moore","year":"1999","unstructured":"Moore, J.S.: A mechanically checked proof of a multiprocessor result via a uniprocessor view. Form. Methods Syst. Des. 14, 213\u2013228 (1999)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"9389_CR38","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"B Moszkowski","year":"1985","unstructured":"Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. IEEE Comput. 18(2), 10\u201319 (1985)","journal-title":"IEEE Comput."},{"key":"9389_CR39","volume-title":"Executing Temporal Logic Programs","author":"B Moszkowski","year":"1986","unstructured":"Moszkowski, B.: Executing Temporal Logic Programs. Cambridge University Press, Cambridge (1986)"},{"key":"9389_CR40","doi-asserted-by":"crossref","unstructured":"Moszkowski, B.: Compositional reasoning about projected and infinite time. In: Proceedings of the 1st ICECCS, pp. 238\u2013245. IEEE Computer Society (1995)","DOI":"10.1109\/ICECCS.1995.479336"},{"key":"9389_CR41","first-page":"223","volume-title":"ICALP \u201900: 1459 Proceedings of the 27th International Colloquium on Automata, Languages and Programming","author":"B Moszkowski","year":"2000","unstructured":"Moszkowski, B.: An automata-theoretic completeness proof for interval temporal logic. In: ICALP \u201900: Proceedings of the 27th International Colloquium on Automata, Languages and Programming, pp. 223\u2013234. Springer-Verlag, London (2000)"},{"issue":"9","key":"9389_CR42","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1016\/j.ipl.2013.02.005","volume":"113","author":"B Moszkowski","year":"2013","unstructured":"Moszkowski, B.: Interconnections between classes of sequentially compositional temporal formulas. Inf. Process. Lett. 113(9), 350\u2013353 (2013)","journal-title":"Inf. Process. Lett."},{"key":"9389_CR43","doi-asserted-by":"crossref","unstructured":"Nafz, F., Seebach, H., Stegh\u00f6fer, J.P., B\u00e4umler, S., Reif, W.: A formal framework for compositional verification of organic computing systems. In: Proceedings of the 7th International Conference on Autonomic and Trusted Computing (ATC 2010), pp. 17\u201331. Springer, LNCS (2010)","DOI":"10.1007\/978-3-642-16576-4_2"},{"issue":"3","key":"9389_CR44","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"9389_CR45","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual IEEE Symposium on the Foundation of Computer Science (FOCS), pp. 46\u201357. IEEE Computer Society Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"9389_CR46","doi-asserted-by":"crossref","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, vol. II, pp. 13\u201339. Kluwer, Dordrecht (1998)","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"9389_CR47","unstructured":"de Roever, W.P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. No. 54 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (2001)"},{"key":"9389_CR48","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Reif, W.: Interleaved programs and rely-guarantee reasoning with ITL. In: Proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME), pp. 99\u2013106. IEEE Computer Society Press (2011)","DOI":"10.1109\/TIME.2011.12"},{"key":"9389_CR49","doi-asserted-by":"crossref","unstructured":"St\u00f8len, K.: A method for the development of totally correct shared-state parallel programs. In: CONCUR\u201991, vol. 527, pp. 510\u2013525. Springer LNCS (1991)","DOI":"10.1007\/3-540-54430-5_110"},{"key":"9389_CR50","doi-asserted-by":"crossref","unstructured":"Tofan, B., B\u00e4umler, S., Schellhorn, G., Reif, W.: Temporal logic verification of lock-freedom. In: Proceedings of MPC 2010, pp. 377\u2013396. Springer LNCS 6120 (2010)","DOI":"10.1007\/978-3-642-13321-3_21"},{"key":"9389_CR51","unstructured":"Tofan, B., Schellhorn, G., Ernst, G., Pf\u00e4hler, J., Reif, W.: Compositional Verification of a Lock-Free Stack with RGITL. In: Proceedings of International Workshop on Automated Verification of Critical Systems (to appear in ECEASST) (2013)"},{"key":"9389_CR52","doi-asserted-by":"crossref","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: Formal verification of a lock-free stack with hazard pointers. In: Proceedings ICTAC, pp. 239\u2013255. Springer LNCS 6916 (2011)","DOI":"10.1007\/978-3-642-23283-1_16"},{"key":"9389_CR53","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Parkinson, M.J.: A marriage of rely\/guarantee and separation logic. In: CONCUR, vol. 4703, pp. 256\u2013271. Springer LNCS (2007)","DOI":"10.1007\/978-3-540-74407-8_18"},{"issue":"2","key":"9389_CR54","first-page":"149","volume":"9","author":"Q Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. FAC J. 9(2), 149\u2013174 (1997)","journal-title":"FAC J."},{"key":"9389_CR55","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1007\/3-540-49213-5_22","volume":"1536","author":"Q Xu","year":"1998","unstructured":"Xu, Q., Swarup, M.: Compositional reasoning using the assumption-commitment paradigm. Lect. Notes Comput. Sci. 1536, 565\u2013583 (1998)","journal-title":"Lect. Notes Comput. Sci."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-013-9389-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-013-9389-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-013-9389-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T17:57:11Z","timestamp":1746122231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-013-9389-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,29]]},"references-count":55,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["9389"],"URL":"https:\/\/doi.org\/10.1007\/s10472-013-9389-z","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,1,29]]}}}