{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:53:36Z","timestamp":1762458816812},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642133206"},{"type":"electronic","value":"9783642133213"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-13321-3_4","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T02:24:11Z","timestamp":1277173451000},"page":"22-41","source":"Crossref","is-referenced-by-count":8,"title":["On Automated Program Construction and Verification"],"prefix":"10.1007","author":[{"given":"Rudolf","family":"Berghammer","sequence":"first","affiliation":[]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"4_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R.-J. Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)"},{"key":"4_CR3","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":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/3-540-36280-0_17","volume-title":"Relational Methods in Computer Science","author":"R. Berghammer","year":"2002","unstructured":"Berghammer, R., Leoniuk, B., Milanese, U.: Implementation of Relation Algebra using Binary Decision Diagrams. In: de Swart, H. (ed.) RelMiCS 2001. LNCS, vol.\u00a02561, pp. 241\u2013257. Springer, Heidelberg (2002)"},{"key":"4_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":"4_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 Informatica\u00a045, 211\u2013236 (2008)","journal-title":"Acta Informatica"},{"key":"4_CR7","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, D.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)","edition":"3"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-540-70594-9_19","volume-title":"Mathematics of Program Construction","author":"J. Desharnais","year":"2008","unstructured":"Desharnais, J., Struth, G.: Modal Semirings Revisited. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol.\u00a05133, pp. 360\u2013387. Springer, Heidelberg (2008)"},{"key":"4_CR9","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning Meanings to Programs. In: Proc. AMS Symposia on Applied Mathematics, vol.\u00a019, pp. 19\u201331 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"4_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Computer Programming","author":"D. Gries","year":"1981","unstructured":"Gries, D.: The Science of Computer Programming. Springer, Heidelberg (1981)"},{"issue":"10","key":"4_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"4_CR13","unstructured":"H\u00f6fner, P., Struth, G.: Algebraic Reasoning with Prover9 (2009), \n                    \n                      www.dcs.shef.ac.uk\/~georg\/ka\/"},{"key":"4_CR14","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, P. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 279\u2013294. Springer, Heidelberg (2007)"},{"key":"4_CR15","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":"4_CR16","volume-title":"Software Abstractions","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions. The MIT Press, Cambridge (2006)"},{"issue":"3","key":"4_CR17","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":"4_CR18","volume-title":"Relation Algebras","author":"R.D. Maddux","year":"2006","unstructured":"Maddux, R.D.: Relation Algebras. Elsevier, Amsterdam (2006)"},{"key":"4_CR19","unstructured":"McCune, W.: Prover9 and Mace4 (2007), \n                    \n                      www.prover9.org"},{"key":"4_CR20","unstructured":"Ng, J.: Relation Algebras with Transitive Closure. Ph.D. thesis, University of California, Berkeley (1984)"},{"key":"4_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-77968-8","volume-title":"Relations and Graphs","author":"G. Schmidt","year":"1993","unstructured":"Schmidt, G., Str\u00f6hlein, T.: Relations and Graphs. Springer, Heidelberg (1993)"},{"key":"4_CR22","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"2006","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall, Englewood Cliffs (2006)"},{"key":"4_CR23","doi-asserted-by":"crossref","first-page":"386","DOI":"10.4064\/fm-16-1-386-389","volume":"16","author":"E. Szpilrajn","year":"1930","unstructured":"Szpilrajn, E.: Sur l\u2019extension de l\u2019ordre partiel. Fundamenta Math.\u00a016, 386\u2013389 (1930)","journal-title":"Fundamenta Math."},{"key":"4_CR24","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. Symbolic Logic\u00a06, 73\u201389 (1941)","journal-title":"J. Symbolic Logic"},{"key":"4_CR25","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/321105.321107","volume":"9","author":"S. Warshall","year":"1962","unstructured":"Warshall, S.: A Theorem on Boolean Matrices. Journal of the ACM\u00a09, 11\u201312 (1962)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-13321-3_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T08:01:32Z","timestamp":1619769692000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-13321-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642133206","9783642133213"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-13321-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}