{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:00:08Z","timestamp":1762459208300,"version":"3.40.4"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319062501"},{"type":"electronic","value":"9783319062518"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06251-8_11","type":"book-chapter","created":{"date-parts":[[2014,4,8]],"date-time":"2014-04-08T01:32:39Z","timestamp":1396920759000},"page":"173-190","source":"Crossref","is-referenced-by-count":5,"title":["Automated Verification of Relational While-Programs"],"prefix":"10.1007","author":[{"given":"Rudolf","family":"Berghammer","sequence":"first","affiliation":[]},{"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[]},{"given":"Insa","family":"Stucke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0020-0255(99)00012-2","volume":"119","author":"R. Berghammer","year":"1999","unstructured":"Berghammer, R.: Combining relational calculus and the Dijkstra-Gries method for deriving relational programs. Information Sciences\u00a0119, 155\u2013171 (1999)","journal-title":"Information Sciences"},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0167-6423(99)00043-X","volume":"38","author":"R. Berghammer","year":"2000","unstructured":"Berghammer, R., Hoffmann, T.: Deriving relational programs for computing kernels by reconstructing a proof of Richardson\u2019s theorem. Science of Computer Programming\u00a038, 1\u201325 (2000)","journal-title":"Science of Computer Programming"},{"key":"11_CR3","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0020-0255(01)00163-3","volume":"139","author":"R. Berghammer","year":"2001","unstructured":"Berghammer, R., Hoffmann, T.: Relational depth-first-search with applications. Information Sciences\u00a0139, 167\u2013186 (2001)","journal-title":"Information Sciences"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/s00236-008-0072-5","volume":"45","author":"R. Berghammer","year":"2008","unstructured":"Berghammer, R.: Applying relation algebra and Rel View to solve problems on orders and lattices. Acta Informatica\u00a045, 211\u2013236 (2008)","journal-title":"Acta Informatica"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-13321-3_4","volume-title":"Mathematics of Program Construction","author":"R. Berghammer","year":"2010","unstructured":"Berghammer, R., Struth, G.: On automated program construction and verification. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol.\u00a06120, pp. 22\u201341. Springer, Heidelberg (2010)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Berghammer, R., Fischer, S.: Simple rectangle-based functional programs for computing reflexive-transitive closures. In: Kahl, W., Griffin, T.G. (eds.) RAMiCS 2012. LNCS, vol.\u00a07560, pp. 114\u2013129. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-33314-9_8"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Bibel, W., Schmitt, P.: Automated deduction: A basis for applications. Applied Logic Series. Kluwer (1998)","DOI":"10.1007\/978-94-017-0437-3"},{"key":"11_CR8","first-page":"341","volume":"1","author":"L.H. Chin","year":"1951","unstructured":"Chin, L.H., Tarski, A.: Distributive and modular laws in the arithmetic of relation algebras. Univ. of California Publ. Math. (new series)\u00a01, 341\u2013384 (1951)","journal-title":"Univ. of California Publ. Math. (new series)"},{"key":"11_CR9","unstructured":"Dang, H.H., H\u00f6fner, P.: First-order theorem prover evaluation w.r.t. relation- and Kleene algebra. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) Relations and Kleene Algebra in Computer Science \u2013 Ph.D. Programme at RelMiCS 10\/AKA 05. Technical Report 2008-04, Institut f\u00fcr Informatik, Universit\u00e4t Augsburg, 48-52 (2008)"},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM\u00a018, 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"11_CR11","unstructured":"Dijkstra, E.W.: A discipline of programming. Prentice-Hall (1976)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Foster, S., Struth, G., Weber, T.: Automated engineering of relational and algebraic methods in Isabelle\/HOL (invited Tutorial). In: de Swart, H. (ed.) RAMiCS 2011. LNCS, vol.\u00a06663, pp. 52\u201367. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-21070-9_5"},{"key":"11_CR13","unstructured":"Gries, D.: The science of computer programming. Springer (1981)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Hattensperger, C., Berghammer, R., Schmidt, G.: RALF \u2013 A relation-algebraic formula manipulation system and proof checker. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Algebraic Methodology and Software Technology. Workshops in Computing, pp. 407\u2013408. Springer (1993)","DOI":"10.1007\/978-1-4471-3227-1_44"},{"key":"11_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-73595-3_19","volume-title":"Automated Deduction \u2013 CADE-21","author":"P. H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Automated reasoning in Kleene Algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 279\u2013294. Springer, Heidelberg (2007)"},{"key":"11_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-71070-7_5","volume-title":"Automated Reasoning","author":"P. H\u00f6fner","year":"2008","unstructured":"H\u00f6fner, P., Struth, G.: On automating the calculus of relations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 50\u201366. Springer, Heidelberg (2008)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Kahl, W.: Calculational relation-algebraic proofs in Isabelle\/Isar. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS\/Kleene-Algebra Ws 2003. LNCS, vol.\u00a03051, pp. 178\u2013190. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24771-5_16"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/368996.369025","volume":"5","author":"A.B. Kahn","year":"1962","unstructured":"Kahn, A.B.: Topological sorting of large networks. Communications of the ACM\u00a05, 558\u2013562 (1962)","journal-title":"Communications of the ACM"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L.: Invariant generation for P-solvable loops with assignments. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds.) CSR 2008. LNCS, vol.\u00a05010, pp. 349\u2013359. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-79709-8_35"},{"issue":"3","key":"11_CR20","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1023\/A:1020572931854","volume":"71","author":"W. MacCaull","year":"2002","unstructured":"MacCaull, W., Or\u0142owska, E.: Correspondence results for relational proof systems with application to the Lambek calculus. Studia Logica\u00a071(3), 389\u2013414 (2002)","journal-title":"Studia Logica"},{"issue":"5","key":"11_CR21","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","volume":"91","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Computing polynomial program invariants. Information Processing Letters\u00a091(5), 233\u2013244 (2004)","journal-title":"Information Processing Letters"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Schmidt, G., Str\u00f6hlein, T.: Relations and graphs, Discrete mathematics for computer scientists. EATCS Monographs on Theoretical Computer Science. Springer (1993)","DOI":"10.1007\/978-3-642-77968-8"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Schmidt, G.: Relational mathematics. Encyclopedia of Mathematics and its Applications, vol.\u00a0132. Cambridge University Press (2010)","DOI":"10.1017\/CBO9780511778810"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Schumann, J.: Automated theorem proving in software engineering. Springer (2001)","DOI":"10.1007\/978-3-662-22646-9"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Sinz, C.: System description: ARA \u2013 An automated theorem prover for relation algebras. In: McAllester, D. (ed.) CADE-17. LNCS (LNAI), vol.\u00a01831, pp. 177\u2013182. Springer, Heidelberg (2000)","DOI":"10.1007\/10721959_13"},{"issue":"3","key":"11_CR26","doi-asserted-by":"publisher","first-page":"73","DOI":"10.2307\/2268577","volume":"6","author":"A. Tarski","year":"1941","unstructured":"Tarski, A.: On the calculus of relations. Journal of Symbolic Logic\u00a06(3), 73\u201389 (1941)","journal-title":"Journal of Symbolic Logic"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Tarski, A., Givant, S.: A formalization of set theory without variables, vol.\u00a041. AMS Colloquium Publications (1987)","DOI":"10.1090\/coll\/041"},{"key":"11_CR28","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-63104-6_36","volume-title":"Automated Deduction - CADE-14","author":"D. Oheimb von","year":"1997","unstructured":"von Oheimb, D., Gritzner, T.F.: RALL: Machine-supported proofs for relation algebra. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 380\u2013394. Springer, Heidelberg (1997)"},{"key":"11_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System description: SPASS version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"},{"key":"11_CR30","unstructured":"Rel View homepage: http:\/\/www.informatik.uni-kiel.de\/~progsys\/relview\/ (accessed April 30, 2013)"},{"key":"11_CR31","unstructured":"McCune, W.W.: Prover9 and Mace4., http:\/\/www.cs.unm.edu\/~mccune\/prover9 (accessed April 30, 2013)"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06251-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T09:07:14Z","timestamp":1746176834000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06251-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319062501","9783319062518"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06251-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}