{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:56:18Z","timestamp":1762458978855,"version":"3.40.3"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2012,7,13]],"date-time":"2012-07-13T00:00:00Z","timestamp":1342137600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s00236-012-0162-2","type":"journal-article","created":{"date-parts":[[2012,7,12]],"date-time":"2012-07-12T08:40:37Z","timestamp":1342082437000},"page":"343-359","source":"Crossref","is-referenced-by-count":11,"title":["Algebras for iteration and infinite computations"],"prefix":"10.1007","volume":"49","author":[{"given":"Walter","family":"Guttmann","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,7,13]]},"reference":[{"issue":"3","key":"162_CR1","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0020-0190(94)00195-5","volume":"53","author":"C.J. Aarts","year":"1995","unstructured":"Aarts C.J., Backhouse R.C., Boiten E.A., Doornbos H., van Gasteren N., van Geldrop R., Hoogendijk P.F., Voermans E., van der Woude J.: Fixed-point calculus. Inf. Process. Lett. 53(3), 131\u2013136 (1995)","journal-title":"Inf. Process. Lett."},{"key":"162_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"K.R. Apt","year":"2009","unstructured":"Apt K.R., de Boer F.S., Olderog E.-R.: Verification of Sequential and Concurrent Programs. 3rd edn. Springer, London (2009)","edition":"3"},{"issue":"4","key":"162_CR3","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/s002360050163","volume":"36","author":"R.J.R. Back","year":"1999","unstructured":"Back R.J.R., von Wright J.: Reasoning algebraically about loops. Acta Informatica 36(4), 295\u2013334 (1999)","journal-title":"Acta Informatica"},{"key":"162_CR4","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(86)90172-6","volume":"43","author":"R. Berghammer","year":"1986","unstructured":"Berghammer R., Zierer H.: Relational algebraic semantics of deterministic and nondeterministic programs. Theor. Comput. Sci. 43, 123\u2013147 (1986)","journal-title":"Theor. Comput. Sci."},{"key":"162_CR5","volume-title":"Lattice Theory, volume XXV of Colloquium Publications","author":"G. Birkhoff","year":"1967","unstructured":"Birkhoff G.: Lattice Theory, volume XXV of Colloquium Publications. 3rd edn. American Mathematical Society, Providence, RI (1967)","edition":"3"},{"key":"162_CR6","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction: CADE-23, volume 6803 of Lecture Notes in Computer Science","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette J.C., B\u00f6hme S., Paulson L.C.: Extending Sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction: CADE-23, volume 6803 of Lecture Notes in Computer Science, pp. 116\u2013130. Springer, Berlin (2011)"},{"key":"162_CR7","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science","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.) Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pp. 131\u2013146. Springer, Berlin (2010)"},{"key":"162_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-78034-9","volume-title":"Iteration Theories: The Equational Logic of Iterative Processes","author":"S.L. Bloom","year":"1993","unstructured":"Bloom S.L., \u00c9sik Z.: Iteration Theories: The Equational Logic of Iterative Processes. Springer, Berlin (1993)"},{"key":"162_CR9","first-page":"553","volume-title":"Program Construction, volume 69 of Lecture Notes in Computer Science","author":"M. Broy","year":"1979","unstructured":"Broy M., Gnatz R., Wirsing M.: Semantics of nondeterministic and noncontinuous constructs. In: Bauer, F.L., Broy, M. (eds.) Program Construction, volume 69 of Lecture Notes in Computer Science, pp. 553\u2013592. Springer, Berlin (1979)"},{"key":"162_CR10","first-page":"45","volume-title":"Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science","author":"E. Cohen","year":"2000","unstructured":"Cohen E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pp. 45\u201359. Springer, Berlin (2000)"},{"key":"162_CR11","volume-title":"Regular Algebra and Finite Machines","author":"J.H. Conway","year":"1971","unstructured":"Conway J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)"},{"key":"162_CR12","first-page":"435","volume-title":"Automata, Languages and Programming: Third International Colloquium","author":"J.W. Bakker de","year":"1976","unstructured":"de Bakker J.W.: Semantics and termination of nondeterministic recursive programs. In: Michaelson, S., Milner, R. (eds.) Automata, Languages and Programming: Third International Colloquium, pp. 435\u2013477. Edinburgh University Press, Edinburgh (1976)"},{"key":"162_CR13","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/11828563_8","volume-title":"Relations and Kleene Algebra in Computer Science, volume 4136 of Lecture Notes in Computer Science","author":"J.-L. De Carufel","year":"2006","unstructured":"De Carufel J.-L., Desharnais J.: Demonic algebra with domain. In: Schmidt, R. (ed) Relations and Kleene Algebra in Computer Science, volume 4136 of Lecture Notes in Computer Science, pp. 120\u2013134. Springer, Berlin (2006)"},{"issue":"4","key":"162_CR14","doi-asserted-by":"crossref","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 Trans. Comput. Log. 7(4), 798\u2013833 (2006)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1:1","key":"162_CR15","first-page":"1","volume":"7","author":"J. Desharnais","year":"2011","unstructured":"Desharnais J., M\u00f6ller B., Struth G.: Algebraic notions of termination. Log. Methods Comput. Sci. 7(1:1), 1\u201329 (2011)","journal-title":"Log. Methods Comput. Sci."},{"issue":"2","key":"162_CR16","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/j.jlap.2005.04.006","volume":"66","author":"J. Desharnais","year":"2006","unstructured":"Desharnais J., M\u00f6ller B., Tchier F.: Kleene under a modal demonic star. J. Log. Algebr. Program. 66(2), 127\u2013160 (2006)","journal-title":"J. Log. Algebr. Program."},{"issue":"3","key":"162_CR17","doi-asserted-by":"crossref","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":"162_CR18","first-page":"363","volume-title":"Programming Concepts, Methods and Calculi","author":"H. Doornbos","year":"1994","unstructured":"Doornbos H.: A relational model of programs without the restriction to Egli-Milner-monotone constructs. In: Olderog, E.-R. (ed.) Programming Concepts, Methods and Calculi, pp. 363\u2013382. North-Holland Publishing Company, Amsterdam (1994)"},{"key":"162_CR19","doi-asserted-by":"crossref","unstructured":"Dunne, S.: Recasting Hoare and He\u2019s unifying theory of programs in the context of general correctness. In: Butterfield, A., Strong, G., Pahl, C. (eds.) 5th Irish Workshop on Formal Methods, Electronic Workshops in Computing. The British Computer Society (2001)","DOI":"10.14236\/ewic\/IWFM2001.1"},{"key":"162_CR20","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1007\/978-3-642-04639-1_11","volume-title":"Relations and Kleene Algebra in Computer Science, volume 5827 of Lecture Notes in Computer Science","author":"W. Guttmann","year":"2009","unstructured":"Guttmann W.: General correctness algebra. In: Berghammer, R., Jaoua, A.M., M\u00f6ller, B. (eds.) Relations and Kleene Algebra in Computer Science, volume 5827 of Lecture Notes in Computer Science, pp. 150\u2013165. Springer, Berlin (2009)"},{"key":"162_CR21","first-page":"157","volume-title":"Mathematics of Program Construction, volume 6120 of Lecture Notes in Computer Science","author":"W. Guttmann","year":"2010","unstructured":"Guttmann W.: Partial, total and general correctness. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) Mathematics of Program Construction, volume 6120 of Lecture Notes in Computer Science, pp. 157\u2013177. Springer, Berlin (2010)"},{"key":"162_CR22","doi-asserted-by":"crossref","unstructured":"Guttmann, W.: Unifying recursion in partial, total and general correctness. In: Qin, S. (eds.) Unifying Theories of Programming, Third International Symposium, UTP 2010, volume 6445 of Lecture Notes in Computer Science, pp. 207\u2013225. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16690-7_10"},{"issue":"6","key":"162_CR23","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1016\/j.jlap.2011.04.004","volume":"80","author":"W. Guttmann","year":"2011","unstructured":"Guttmann W.: Fixpoints for general correctness. J. Log. Algebr. Program. 80(6), 248\u2013265 (2011)","journal-title":"J. Log. Algebr. Program."},{"key":"162_CR24","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/978-3-642-21070-9_16","volume-title":"Relational and Algebraic Methods in Computer Science, volume 6663 of Lecture Notes in Computer Science","author":"W. Guttmann","year":"2011","unstructured":"Guttmann W.: Towards a typed omega algebra. In: de Swart, H. (ed.) Relational and Algebraic Methods in Computer Science, volume 6663 of Lecture Notes in Computer Science, pp. 196\u2013211. Springer, Berlin (2011)"},{"key":"162_CR25","unstructured":"Guttmann, W.: Extended designs algebraically. Sci. Comput. Program. (2012) (to appear)"},{"key":"162_CR26","first-page":"198","volume-title":"Mathematics of Program Construction, volume 7342 of Lecture Notes in Computer Science","author":"W. Guttmann","year":"2012","unstructured":"Guttmann W.: Unifying correctness statements. In: Gibbons, J., Nogueira, P. (eds.) Mathematics of Program Construction, volume 7342 of Lecture Notes in Computer Science, pp. 198\u2013219. Springer, Berlin (2012)"},{"key":"162_CR27","doi-asserted-by":"crossref","unstructured":"Guttmann, W.: Unifying lazy and strict computations. In: Griffin, T.G., Kahl, W. (eds.) Relational and Algebraic Methods in Computer Science, Lecture Notes in Computer Science. Springer, Berlin (2012) (to appear)","DOI":"10.1007\/978-3-642-33314-9_2"},{"key":"162_CR28","first-page":"236","volume-title":"Unifying Theories of Programming, volume 4010 of Lecture Notes in Computer Science","author":"W. Guttmann","year":"2006","unstructured":"Guttmann W., M\u00f6ller B.: Modal design algebra. In: Dunne, S., Stoddart, W. (eds.) Unifying Theories of Programming, volume 4010 of Lecture Notes in Computer Science, pp. 236\u2013256. Springer, Berlin (2006)"},{"issue":"2","key":"162_CR29","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1016\/j.jlap.2009.07.002","volume":"79","author":"W. Guttmann","year":"2010","unstructured":"Guttmann W., M\u00f6ller B.: Normal design algebra. J. Log. Algebr. Program. 79(2), 144\u2013173 (2010)","journal-title":"J. Log. Algebr. Program."},{"key":"162_CR30","first-page":"617","volume-title":"Formal Methods and Software Engineering, volume 6991 of Lecture Notes in Computer Science","author":"W. Guttmann","year":"2011","unstructured":"Guttmann W., Struth G., Weber T.: Automating algebraic methods in Isabelle. In: Qin, S., Qiu, Z. (eds.) Formal Methods and Software Engineering, volume 6991 of Lecture Notes in Computer Science, pp. 617\u2013632. Springer, Berlin (2011)"},{"key":"162_CR31","first-page":"178","volume-title":"Mathematics of Program Construction, volume 6120 of Lecture Notes in Computer Science","author":"I.J. Hayes","year":"2010","unstructured":"Hayes I.J., Dunne S.E., Meinicke L.: Unifying theories of programming that distinguish nontermination and abort. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) Mathematics of Program Construction, volume 6120 of Lecture Notes in Computer Science, pp. 178\u2013194. Springer, Berlin (2010)"},{"key":"162_CR32","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall Europe (1998)","DOI":"10.1007\/BFb0002714"},{"key":"162_CR33","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/11828563_15","volume-title":"Relations and Kleene Algebra in Computer Science, volume 4136 of Lecture Notes in Computer Science","author":"P. H\u00f6fner","year":"2006","unstructured":"H\u00f6fner P., M\u00f6ller B., Solin K.: Omega algebra, demonic refinement algebra and commands. In: Schmidt, R. (ed.) Relations and Kleene Algebra in Computer Science, volume 4136 of Lecture Notes in Computer Science, pp. 222\u2013234. Springer, Berlin (2006)"},{"issue":"1","key":"162_CR34","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/BF00290146","volume":"22","author":"D. Jacobs","year":"1985","unstructured":"Jacobs D., Gries D.: General correctness: a unification of partial and total correctness. Acta Informatica 22(1), 67\u201383 (1985)","journal-title":"Acta Informatica"},{"issue":"2","key":"162_CR35","doi-asserted-by":"crossref","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. Inf. Comput. 110(2), 366\u2013390 (1994)","journal-title":"Inf. Comput."},{"issue":"3","key":"162_CR36","doi-asserted-by":"crossref","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":"162_CR37","doi-asserted-by":"crossref","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":"162_CR38","unstructured":"McCune, W.: Mace4 reference manual and guide. Technical Memorandum ANL\/MCS-TM-264, Mathematics and Computer Science Division, Argonne National Laboratory, (2003). Mace4 is available at http:\/\/www.cs.unm.edu\/~mccune\/mace4\/"},{"key":"162_CR39","first-page":"338","volume-title":"Mathematics of Program Construction, volume 4014 of Lecture Notes in Computer Science","author":"B. M\u00f6ller","year":"2006","unstructured":"M\u00f6ller B.: The linear algebra of UTP. In: Uustalu, T. (ed.) Mathematics of Program Construction, volume 4014 of Lecture Notes in Computer Science, pp. 338\u2013358. Springer, Berlin (2006)"},{"issue":"2","key":"162_CR40","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/j.scico.2006.01.010","volume":"65","author":"B. M\u00f6ller","year":"2007","unstructured":"M\u00f6ller B.: Kleene getting lazy. Sci. Comput. Program. 65(2), 195\u2013214 (2007)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"162_CR41","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 351(2), 221\u2013239 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"162_CR42","first-page":"200","volume-title":"Relational Methods in Computer Science 2005, volume 3929 of Lecture Notes 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.) Relational Methods in Computer Science 2005, volume 3929 of Lecture Notes in Computer Science, pp. 200\u2013211. Springer, Berlin (2006)"},{"issue":"4","key":"162_CR43","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G. Nelson","year":"1989","unstructured":"Nelson G.: A generalization of Dijkstra\u2019s calculus. ACM Trans. Program. Lang. Syst. 11(4), 517\u2013561 (1989)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"8","key":"162_CR44","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1145\/358161.358168","volume":"26","author":"D. Parnas","year":"1983","unstructured":"Parnas D.: A generalized control structure and its formal definition. Commun. ACM 26(8), 572\u2013581 (1983)","journal-title":"Commun. ACM"},{"key":"162_CR45","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe G., Ternovska E., Schulz S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics, pp. 3\u201313 (2010)"},{"issue":"1\u20132","key":"162_CR46","doi-asserted-by":"crossref","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."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-012-0162-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-012-0162-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-012-0162-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T23:04:28Z","timestamp":1743721468000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-012-0162-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,13]]},"references-count":46,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["162"],"URL":"https:\/\/doi.org\/10.1007\/s00236-012-0162-2","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2012,7,13]]}}}