{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:02:26Z","timestamp":1762459346642},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319247038"},{"type":"electronic","value":"9783319247045"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24704-5_17","type":"book-chapter","created":{"date-parts":[[2015,9,24]],"date-time":"2015-09-24T01:31:29Z","timestamp":1443058289000},"page":"275-292","source":"Crossref","is-referenced-by-count":3,"title":["Tool-Based Verification of a Relational Vertex Coloring Program"],"prefix":"10.1007","author":[{"given":"Rudolf","family":"Berghammer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Insa","family":"Stucke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"unstructured":"Armstrong, A., Foster, S., Struth, G., Weber, T.: Relation algebra. Archive of Formal Proofs (2014). \n                      \n                        http:\/\/afp.sf.net\/entries\/Relation_Algebra.shtml","key":"17_CR1"},{"key":"17_CR2","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. Inform. Sci.\u00a0119, 155\u2013171 (1999)","journal-title":"Inform. Sci."},{"key":"17_CR3","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. Sci. Comput, Prog.\u00a038, 1\u201325 (2000)","journal-title":"Sci. Comput, Prog."},{"key":"17_CR4","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. Inform. Sci.\u00a0139, 167\u2013186 (2001)","journal-title":"Inform. Sci."},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/11555964_4","volume-title":"Computer Algebra in Scientific Computing","author":"R. Berghammer","year":"2005","unstructured":"Berghammer, R., Neumann, F.: RelView \u2013 An OBDD-based Computer Algebra system for relations. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2005. LNCS, vol.\u00a03718, pp. 40\u201351. Springer, Heidelberg (2005)"},{"key":"17_CR6","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 RelView to solve problems on orders and lattices. Acta Inform.\u00a045, 211\u2013236 (2008)","journal-title":"Acta Inform."},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s00236-009-0109-4","volume":"47","author":"R. Berghammer","year":"2010","unstructured":"Berghammer, R., Winter, M.: Embedding mappings and splittings with applications. Acta Inform.\u00a047, 77\u2013110 (2010)","journal-title":"Acta Inform."},{"key":"17_CR8","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":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-319-06251-8_19","volume-title":"Relational and Algebraic Methods in Computer Science","author":"R. Berghammer","year":"2014","unstructured":"Berghammer, R., H\u00f6fner, P., Stucke, I.: Automated verification of relational while-programs. In: H\u00f6fner, P., Jipsen, P., Kahl, W., M\u00fcller, M.E. (eds.) RAMiCS 2014. LNCS, vol.\u00a08428, pp. 309\u2013326. Springer, Heidelberg (2014)"},{"unstructured":"Berghammer, R., Stucke, I., Winter, M.: Investigating and computing bipartitions with algebraic means. In: Kahl, W., Oliviera, J.N., Winter, M. (eds.) Relational and Algebraic Methods in Computer Science (to appear)","key":"17_CR10"},{"doi-asserted-by":"crossref","unstructured":"Bertot, Y., Casteran, P.: Interactive theorem proving and program development. Coq\u2019Art: The calculus of inductive constructions. Texts in Theoretical Computer Science. Springer (2004)","key":"17_CR11","DOI":"10.1007\/978-3-662-07964-5"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","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.) CADE 2011. LNCS, vol.\u00a06803, pp. 116\u2013130. Springer, Heidelberg (2011)"},{"key":"17_CR13","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)"},{"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 RelMiCS10\/AKA05. Technical Report 2008-04, Institut f\u00fcr Informatik, Universit\u00e4t Augsburg, 48\u201352 (2008)","key":"17_CR14"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-21070-9_5","volume-title":"Relational and Algebraic Methods in Computer Science","author":"S. Foster","year":"2011","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)"},{"key":"17_CR16","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":"17_CR17","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":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-540-24771-5_16","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"W. Kahl","year":"2004","unstructured":"Kahl, W.: Calculational relation-algebraic proofs in Isabelle\/Isar. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol.\u00a03051, pp. 179\u2013190. Springer, Heidelberg (2004)"},{"unstructured":"Maddux, R.: Relation algebras. Studies in Logic and the Foundations of Mathematics, vol.\u00a0150. Elsevier (2006)","key":"17_CR19"},{"unstructured":"McCune, W.W.: Prover9 and Mace4, \n                      \n                        http:\/\/www.cs.unm.edu\/~mccune\/prover9","key":"17_CR20"},{"key":"17_CR21","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A proof assistant for higher-order logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"17_CR22","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)"},{"unstructured":"Pous, D.: Relation algebra and KAT in Coq, \n                      \n                        http:\/\/perso.ens-lyon.fr\/damien.pous\/ra\/","key":"17_CR23"},{"unstructured":"Schmidt, G., Str\u00f6hlein, T.: Relations and graphs, Discrete mathematics for computer scientists. EATCS Monographs on Theoretical Computer Science. Springer (1993)","key":"17_CR24"},{"doi-asserted-by":"crossref","unstructured":"Schmidt, G.: Relational mathematics. Encyclopedia of Mathematics and its Applications. Cambridge University Press (2010)","key":"17_CR25","DOI":"10.1017\/CBO9780511778810"},{"issue":"3","key":"17_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. J. Symb. Logic\u00a06(3), 73\u201389 (1941)","journal-title":"J. Symb. Logic"},{"doi-asserted-by":"crossref","unstructured":"Tarski, A., Givant, S.: A formalization of set theory without variables. AMS Colloquium Publications, American Mathematical Society (1987)","key":"17_CR27","DOI":"10.1090\/coll\/041"},{"unstructured":"Wenzel, M.: Isabelle\/Isar \u2013 a versatile environment for human-readable formal proof documents. Dissertation, Technische Universit\u00e4t M\u00fcnchen (2002)","key":"17_CR28"},{"unstructured":"Coq-homepage: \n                      \n                        https:\/\/coq.inria.fr","key":"17_CR29"},{"unstructured":"RelView-homepage: \n\t\t\t\t\t\n                      \n                        http:\/\/www.informatik.uni-kiel.de\/~progsys\/relview\/","key":"17_CR30"},{"unstructured":"Why3-homepage: \n                      \n                        http:\/\/why3.lri.fr\/","key":"17_CR31"},{"unstructured":"Input files and proof scripts: \n                      \n                        http:\/\/www.hoefner-online.de\/ramics15\/","key":"17_CR32"}],"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-24704-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:38:55Z","timestamp":1559252335000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24704-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319247038","9783319247045"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24704-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}