{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:41Z","timestamp":1775790701500,"version":"3.50.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319064093","type":"print"},{"value":"9783319064109","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_6","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"78-93","source":"Crossref","is-referenced-by-count":11,"title":["Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools"],"prefix":"10.1007","author":[{"given":"Alasdair","family":"Armstrong","sequence":"first","affiliation":[]},{"given":"Victor B. F.","family":"Gomes","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-319-06251-8_4","volume-title":"RAMiCS","author":"A. Armstrong","year":"2014","unstructured":"Armstrong, A., Gomes, V.B.F., Struth, G.: Algebras for program correctness in isabelle\/HOL. In: Kahl, W. (ed.) RAMiCS 2014. LNCS, vol.\u00a08428, pp. 49\u201364. Springer, Heidelberg (2014)"},{"key":"6_CR2","unstructured":"Armstrong, A., Struth, G., Weber, T.: Kleene algebra. In: Archive of Formal Proofs (2013)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-39634-2_16","volume-title":"Interactive Theorem Proving","author":"A. Armstrong","year":"2013","unstructured":"Armstrong, A., Struth, G., Weber, T.: Program analysis and verification based on Kleene algebra in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 197\u2013212. Springer, Heidelberg (2013)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"J.C. Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 131\u2013146. Springer, Heidelberg (2010)"},{"key":"6_CR5","unstructured":"Brookes, S.: Full abstraction for a shared variable parallel language. In: Okada, M., Panangaden, P. (eds.) LICS, 1993, pp. 98\u2013109 (1993)"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Ong, L. (ed.) LICS 2007, pp. 366\u2013378 (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"6_CR7","unstructured":"Conway, J.H.: Regular algebra and finite machines. Chapman and Hall (1971)"},{"issue":"6","key":"6_CR8","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.jlap.2011.04.003","volume":"80","author":"H.-H. Dang","year":"2011","unstructured":"Dang, H.-H., H\u00f6fner, P., M\u00f6ller, B.: Algebraic separation logic. J. Log. Algebr. Program.\u00a080(6), 221\u2013247 (2011)","journal-title":"J. Log. Algebr. Program."},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1245","DOI":"10.1007\/3-540-48118-4_16","volume-title":"FM\u201999 - Formal Methods","author":"F.S. Boer de","year":"1999","unstructured":"de Boer, F.S., Hannemann, U., de Roever, W.-P.: Formal justification of the rely-guarantee paradigm for shared-variable concurrency: A semantic approach. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1245\u20131265. Springer, Heidelberg (1999)"},{"key":"6_CR10","volume-title":"Concurrency verification: an introduction to state-based methods","author":"W.-P. Roever de","year":"2001","unstructured":"de Roever, W.-P., de Boer, F., Hanneman, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency verification: an introduction to state-based methods. Cambridge University Press, Cambridge (2001)"},{"issue":"2","key":"6_CR11","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s001650200032","volume":"14","author":"J. Dingel","year":"2002","unstructured":"Dingel, J.: A refinement calculus for shared-variable parallel and distributed programming. Formal Aspects of Computing\u00a014(2), 123\u2013197 (2002)","journal-title":"Formal Aspects of Computing"},{"issue":"9","key":"6_CR12","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1145\/358746.358767","volume":"24","author":"J.L. Gischer","year":"1981","unstructured":"Gischer, J.L.: Shuffle languages, Petri nets, and context-sensitive grammars. Commun. ACM\u00a024(9), 597\u2013605 (1981)","journal-title":"Commun. ACM"},{"issue":"2-3","key":"6_CR13","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0304-3975(88)90124-7","volume":"61","author":"J.L. Gischer","year":"1988","unstructured":"Gischer, J.L.: The equational theory of pomsets. Theoretical Computer Science\u00a061(2-3), 199\u2013224 (1988)","journal-title":"Theoretical Computer Science"},{"key":"6_CR14","unstructured":"Hayes, I.J., Jones, C.B., Colvin, R.J.: Refining rely-guarantee thinking (2013) (unpublished)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-23217-6_17","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"C.A.R. Hoare","year":"2011","unstructured":"Hoare, C.A.R., Hussain, A., M\u00f6ller, B., O\u2019Hearn, P.W., Petersen, R.L., Struth, G.: On locality and the exchange law for concurrent processes. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 250\u2013264. Springer, Heidelberg (2011)"},{"issue":"6","key":"6_CR16","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1016\/j.jlap.2011.04.005","volume":"80","author":"T. Hoare","year":"2011","unstructured":"Hoare, T., M\u00f6ller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program.\u00a080(6), 266\u2013296 (2011)","journal-title":"J. Log. Algebr. Program."},{"key":"6_CR17","unstructured":"Jones, C.B.: Development methods for computer programs including a notion of interference. PhD thesis, Oxford University (1981)"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-32347-8_22","volume-title":"Interactive Theorem Proving","author":"G. Klein","year":"2012","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 332\u2013337. Springer, Heidelberg (2012)"},{"issue":"2","key":"6_CR19","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation\u00a0110(2), 366\u2013390 (1994)","journal-title":"Information and Computation"},{"issue":"3","key":"6_CR20","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst.\u00a019(3), 427\u2013443 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Laurence, M.R., Struth, G.: Completeness results for bi-Kleene algebras and regular pomset languages (2013) (submitted)","DOI":"10.1007\/978-3-319-06251-8_5"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-62844-4_28","volume-title":"New Trends in Formal Languages","author":"A. Mateescu","year":"1997","unstructured":"Mateescu, A., Mateescu, G.D., Rozenberg, G., Salomaa, A.: Shuffle-like operations on \u03c9-words. In: P\u0103un, G., Salomaa, A. (eds.) New Trends in Formal Languages. LNCS, vol.\u00a01218, pp. 395\u2013411. Springer, Heidelberg (1997)"},{"issue":"2","key":"6_CR23","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.tcs.2005.09.069","volume":"351","author":"B. M\u00f6ller","year":"2006","unstructured":"M\u00f6ller, B., Struth, G.: Algebras of modal operators and partial correctness. Theoretical Computer Science\u00a0351(2), 221\u2013239 (2006)","journal-title":"Theoretical Computer Science"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-36575-3_24","volume-title":"Programming Languages and Systems","author":"L.P. Nieto","year":"2003","unstructured":"Nieto, L.P.: The rely-guarantee method in Isabelle\/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 348\u2013362. Springer, Heidelberg (2003)"},{"key":"6_CR25","unstructured":"Owicki, S.: Axiomatic Proof Techniques for Parallel Programs. PhD thesis, Cornell University (1975)"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-39634-2_15","volume-title":"Interactive Theorem Proving","author":"D. Pous","year":"2013","unstructured":"Pous, D.: Kleene algebra with tests and Coq tools for while programs. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 180\u2013196. Springer, Heidelberg (2013)"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BFb0018436","volume-title":"Logics in AI","author":"V.R. Pratt","year":"1991","unstructured":"Pratt, V.R.: Action logic and pure induction. In: van Eijck, J. (ed.) JELIA 1990. LNCS, vol.\u00a0478, pp. 97\u2013120. Springer, Heidelberg (1991)"},{"key":"6_CR28","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/0167-6423(85)90004-8","volume":"5","author":"A. Tarlecki","year":"1985","unstructured":"Tarlecki, A.: A language of specified programs. Science of Computer Programming\u00a05, 59\u201381 (1985)","journal-title":"Science of Computer Programming"},{"key":"6_CR29","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. PhD thesis, University of Cambridge (2008)"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T16:42:25Z","timestamp":1558888945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}