{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T01:00:13Z","timestamp":1740099613372,"version":"3.37.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030336356"},{"type":"electronic","value":"9783030336363"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-33636-3_8","type":"book-chapter","created":{"date-parts":[[2019,10,19]],"date-time":"2019-10-19T14:02:20Z","timestamp":1571493740000},"page":"197-225","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Cylindric Kleene Lattices for Program Construction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3649-392X","authenticated-orcid":false,"given":"Ian","family":"Hayes","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5272-820X","authenticated-orcid":false,"given":"Larissa","family":"Meinicke","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,10,20]]},"reference":[{"issue":"52","key":"8_CR1","doi-asserted-by":"publisher","first-page":"7099","DOI":"10.1016\/j.tcs.2011.09.024","volume":"412","author":"H Andr\u00e9ka","year":"2011","unstructured":"Andr\u00e9ka, H., Mikul\u00e1s, S., N\u00e9meti, I.: The equational theory of Kleene lattices. Theoret. Comput. Sci. 412(52), 7099\u20137108 (2011)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"8_CR2","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/s00165-015-0343-1","volume":"28","author":"A Armstrong","year":"2016","unstructured":"Armstrong, A., Gomes, V.B.F., Struth, G.: Building program construction and verification tools from algebraic principles. Formal Aspects Comput. 28(2), 265\u2013293 (2016)","journal-title":"Formal Aspects Comput."},{"key":"8_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement calculus - a systematic introduction","author":"R-J Back","year":"1999","unstructured":"Back, R.-J., von Wright, J.: Refinement calculus - a systematic introduction. Springer, New York (1999). https:\/\/doi.org\/10.1007\/978-1-4612-1674-2"},{"key":"8_CR4","volume-title":"Lattice Theory","author":"G Birkhoff","year":"1940","unstructured":"Birkhoff, G.: Lattice Theory. American Mathematical Society, New York (1940)"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"853","DOI":"10.1007\/s00165-017-0416-4","volume":"29","author":"RJ Colvin","year":"2016","unstructured":"Colvin, R.J., Hayes, I.J., Meinicke, L.A.: Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects Comput. 29, 853\u2013875 (2016)","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"8_CR6","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1016\/j.jlamp.2014.10.002","volume":"84","author":"J Cranch","year":"2015","unstructured":"Cranch, J., Laurence, M.R., Struth, G.: Completeness results for omega-regular algebras. J. Logical Algebric Methods Program. 84(3), 402\u2013425 (2015)","journal-title":"J. Logical Algebric Methods Program."},{"issue":"4","key":"8_CR7","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1145\/1183278.1183285","volume":"7","author":"J Desharnais","year":"2006","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Kleene algebra with domain. ACM TOCL 7(4), 798\u2013833 (2006)","journal-title":"ACM TOCL"},{"issue":"3","key":"8_CR8","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/j.scico.2010.05.007","volume":"76","author":"J Desharnais","year":"2011","unstructured":"Desharnais, J., Struth, G.: Internal axioms for domain semirings. Sci. Comput. Program. 76(3), 181\u2013203 (2011)","journal-title":"Sci. Comput. Program."},{"key":"8_CR9","unstructured":"The Coq development team. The Coq proof assistant reference manual. LogiCal Project. Version 8.0 (2004)"},{"key":"8_CR10","unstructured":"Dongol, B., Gomes, V.F.B., Hayes, I.J., Struth, G.: Partial semigroups and convolution algebras. Arch. Formal Proofs (2017)"},{"key":"8_CR11","unstructured":"Dongol, B., Hayes, I.J., Struth, G.: Relational convolution, generalised modalities and incidence algebras. CoRR, abs\/1702.04603 (2017)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-540-24771-5_10","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"T Ehm","year":"2004","unstructured":"Ehm, T., M\u00f6ller, B., Struth, G.: Kleene modules. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 112\u2013123. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24771-5_10"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-19805-2_25","volume-title":"Foundations of Software Science and Computational Structures","author":"MJ Gabbay","year":"2011","unstructured":"Gabbay, M.J., Ciancia, V.: Freshness and name-restriction in sets of traces with names. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 365\u2013380. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19805-2_25"},{"key":"8_CR14","unstructured":"Giacobazzi, R., Debray, S.K., Levi, G.: A generalized semantics for constraint logic programs. In: FGCS, pp. 581\u2013591 (1992)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-319-48989-6_19","volume-title":"FM 2016: Formal Methods","author":"VBF Gomes","year":"2016","unstructured":"Gomes, V.B.F., Struth, G.: Modal Kleene algebra applied to program correctness. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 310\u2013325. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_19"},{"key":"8_CR16","volume-title":"Specification Case Studies","year":"1993","unstructured":"Hayes, I. (ed.): Specification Case Studies, 2nd edn. Prentice Hall International, Englewood Cliffs (1993)","edition":"2"},{"key":"8_CR17","unstructured":"Henkin, L., Donald Monk, J., Tarski, A.: Cylindric Algebras, Part I., volume 64 of Studies in logic and the foundations of mathematics. North-Holland Pub. Co. (1971)"},{"key":"8_CR18","doi-asserted-by":"crossref","first-page":"78","DOI":"10.7551\/mitpress\/4286.003.0007","volume-title":"Logic and Information Flow","author":"D Kozen","year":"1994","unstructured":"Kozen, D.: On action algebras. In: van Eijk, J., Visser, A. (eds.) Logic and Information Flow, pp. 78\u201388. MIT Press, Cambridge (1994)"},{"issue":"3","key":"8_CR19","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. 19(3), 427\u2013443 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"8_CR20","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D Kozen","year":"2000","unstructured":"Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 1(1), 60\u201376 (2000)","journal-title":"ACM Trans. Comput. Log."},{"key":"8_CR21","unstructured":"Meinicke, L.A., Hayes, I.J.: Handling localisation in rely\/guarantee concurrency: an algebraic approach. arXiv:1907.04005 [cs.LO] (2019)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/11734673_16","volume-title":"Relational Methods in Computer Science","author":"B M\u00f6ller","year":"2006","unstructured":"M\u00f6ller, B., Struth, G.: wp is wlp. In: MacCaull, W., Winter, M., D\u00fcntsch, I. (eds.) RelMiCS 2005. LNCS, vol. 3929, pp. 200\u2013211. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11734673_16"},{"key":"8_CR23","volume-title":"Programming From Specifications","author":"C Morgan","year":"1990","unstructured":"Morgan, C.: Programming From Specifications. Prentice-Hall, Upper Saddle River (1990)"},{"key":"8_CR24","volume-title":"Programming from Specifications","author":"CC Morgan","year":"1994","unstructured":"Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice Hall, Hemel Hempstead (1994)","edition":"2"},{"key":"8_CR25","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. 7998, pp. 180\u2013196. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_15"},{"key":"8_CR26","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 Pratt","year":"1991","unstructured":"Pratt, V.: Action logic and pure induction. In: van Eijck, J. (ed.) JELIA 1990. LNCS, vol. 478, pp. 97\u2013120. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0018436"},{"key":"8_CR27","volume-title":"The Z notation: a reference manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z notation: a reference manual, 2nd edn. Prentice Hall International, Englewood Cliffs (1992)","edition":"2"},{"issue":"6","key":"8_CR28","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1017\/S096012951700007X","volume":"28","author":"G Struth","year":"2018","unstructured":"Struth, G.: Hoare semigroups. Math. Struct. Comput. Sci. 28(6), 775\u2013799 (2018)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1\u20132","key":"8_CR29","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.scico.2003.09.002","volume":"51","author":"J Wright von","year":"2004","unstructured":"von Wright, J.: Towards a refinement algebra. Sci. Comput. Program. 51(1\u20132), 23\u201345 (2004)","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"8_CR30","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1080\/00029890.1976.11994114","volume":"83","author":"C Wells","year":"1976","unstructured":"Wells, C.: Some applications of the wreath product construction. Am. Math. Monthly 83(5), 317\u2013338 (1976)","journal-title":"Am. Math. Monthly"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-33636-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:52:24Z","timestamp":1721893944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-33636-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030336356","9783030336363"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-33636-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MPC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Mathematics of Program Construction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mpc2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.nott.ac.uk\/~pszgmh\/mpc19.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"68% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}