{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T11:23:37Z","timestamp":1720437817852},"reference-count":41,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2014,10,1]],"date-time":"2014-10-01T00:00:00Z","timestamp":1412121600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2018,10,15]],"date-time":"2018-10-15T00:00:00Z","timestamp":1539561600000},"content-version":"vor","delay-in-days":1475,"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1016\/j.scico.2013.07.002","type":"journal-article","created":{"date-parts":[[2013,8,2]],"date-time":"2013-08-02T11:31:30Z","timestamp":1375443090000},"page":"179-210","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/http\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":2,"special_numbering":"PB","title":["Refinement algebra with dual operator"],"prefix":"10.1016","volume":"92","author":[{"given":"Viorel","family":"Preoteasa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2013.07.002_br0010","first-page":"19","article-title":"Assigning meanings to programs","volume":"vol. XIX","author":"Floyd","year":"1967"},{"issue":"10","key":"10.1016\/j.scico.2013.07.002_br0020","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"issue":"8","key":"10.1016\/j.scico.2013.07.002_br0030","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","article-title":"Guarded commands, nondeterminacy and formal derivation of programs","volume":"18","author":"Dijkstra","year":"1975","journal-title":"Commun. ACM"},{"key":"10.1016\/j.scico.2013.07.002_br0040","series-title":"On the correctness of refinement in program development","author":"Back","year":"1978"},{"key":"10.1016\/j.scico.2013.07.002_br0050","article-title":"Correctness Preserving Program Refinements: Proof Theory and Applications","volume":"vol. 131","author":"Back","year":"1980"},{"key":"10.1016\/j.scico.2013.07.002_br0060","series-title":"Refinement Calculus. A Systematic Introduction","author":"Back","year":"1998"},{"key":"10.1016\/j.scico.2013.07.002_br0070","series-title":"Programming from Specifications","author":"Morgan","year":"1990"},{"key":"10.1016\/j.scico.2013.07.002_br0080","article-title":"A Discipline of Programming","author":"Dijkstra","year":"1976"},{"key":"10.1016\/j.scico.2013.07.002_br0090","series-title":"International Symposium on Programming","first-page":"164","article-title":"Another characterization of weakest preconditions","volume":"vol. 137","author":"Guerreiro","year":"1982"},{"key":"10.1016\/j.scico.2013.07.002_br0100","series-title":"Proceedings of the International Conference on Mathematics of Program Construction, 375th Anniversary of the Groningen University","first-page":"139","article-title":"A lattice-theoretical basis for a specification language","author":"Back","year":"1989"},{"key":"10.1016\/j.scico.2013.07.002_br0110","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1007\/BF00259469","article-title":"Duality in specification languages: A lattice-theoretical approach","volume":"27","author":"Back","year":"1990","journal-title":"Acta Inform."},{"key":"10.1016\/j.scico.2013.07.002_br0120","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1145\/256167.256195","article-title":"Kleene algebra with tests","volume":"19","author":"Kozen","year":"1997","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"10.1016\/j.scico.2013.07.002_br0130","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1006\/inco.1994.1037","article-title":"A completeness theorem for Kleene algebras and the algebra of regular events","volume":"110","author":"Kozen","year":"1994","journal-title":"Inf. Comput."},{"key":"10.1016\/j.scico.2013.07.002_br0140","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1145\/1183278.1183285","article-title":"Kleene algebra with domain","volume":"7","author":"Desharnais","year":"2006","journal-title":"ACM Trans. Comput. Log."},{"key":"10.1016\/j.scico.2013.07.002_br0150","series-title":"Proceedings of the 20th International Conference on Concurrency Theory","first-page":"399","article-title":"Concurrent Kleene algebra","author":"Hoare","year":"2009"},{"issue":"6","key":"10.1016\/j.scico.2013.07.002_br0160","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/j.jlap.2011.04.003","article-title":"Algebraic separation logic","volume":"80","author":"Dang","year":"2011","journal-title":"J. Log. Algebr. Program."},{"issue":"2","key":"10.1016\/j.scico.2013.07.002_br0170","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/j.tcs.2005.09.069","article-title":"Algebras of modal operators and partial correctness","volume":"351","author":"M\u00f6ller","year":"2006","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10.1016\/j.scico.2013.07.002_br0180","article-title":"Algebraic notions of termination","volume":"7","author":"Desharnais","year":"2011","journal-title":"Log. Methods Comput. Sci."},{"key":"10.1016\/j.scico.2013.07.002_br0190","series-title":"Proceedings of the 6th International Conference on Mathematics of Program Construction","first-page":"233","article-title":"From Kleene algebra to refinement algebra","author":"von Wright","year":"2002"},{"key":"10.1016\/j.scico.2013.07.002_br0200","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.scico.2003.09.002","article-title":"Towards a refinement algebra","volume":"51","author":"von Wright","year":"2004","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.scico.2013.07.002_br0210","doi-asserted-by":"crossref","first-page":"654","DOI":"10.1016\/j.scico.2007.11.004","article-title":"Enabledness and termination in refinement algebra","volume":"74","author":"Solin","year":"2009","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.scico.2013.07.002_br0220","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s00165-009-0111-1","article-title":"Refinement algebra for probabilistic programs","volume":"22","author":"Meinicke","year":"2010","journal-title":"Form. Asp. Comput."},{"key":"10.1016\/j.scico.2013.07.002_br0230","series-title":"Relations and Kleene Algebra in Computer Science","first-page":"373","article-title":"On two dually nondeterministic refinement algebras","volume":"vol. 4136","author":"Solin","year":"2006"},{"key":"10.1016\/j.scico.2013.07.002_br0240","series-title":"Abstract algebra of program refinement","author":"Solin","year":"2007"},{"key":"10.1016\/j.scico.2013.07.002_br0250","series-title":"Formal Methods, Foundations and Applications","first-page":"140","article-title":"Algebra of monotonic boolean transformers","volume":"vol. 7021","author":"Preoteasa","year":"2011"},{"key":"10.1016\/j.scico.2013.07.002_br0260","article-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","volume":"vol. 2283","author":"Nipkow","year":"2002"},{"key":"10.1016\/j.scico.2013.07.002_br0270","author":"Preoteasa"},{"key":"10.1016\/j.scico.2013.07.002_br0280","series-title":"Introduction to Lattices and Order","author":"Davey","year":"2002"},{"key":"10.1016\/j.scico.2013.07.002_br0290","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice-theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pacific J. Math."},{"key":"10.1016\/j.scico.2013.07.002_br0300","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s00165-004-0060-7","article-title":"An algebraic treatment of procedure refinement to support mechanical verification","volume":"17","author":"Back","year":"2005","journal-title":"Form. Asp. Comput."},{"key":"10.1016\/j.scico.2013.07.002_br0310","series-title":"Program variables \u2013 the core of mechanical reasoning about imperative programs","author":"Preoteasa","year":"2006"},{"issue":"42","key":"10.1016\/j.scico.2013.07.002_br0320","doi-asserted-by":"crossref","first-page":"4216","DOI":"10.1016\/j.tcs.2009.05.016","article-title":"Frame rule for mutually recursive procedures manipulating pointers","volume":"410","author":"Preoteasa","year":"2009","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.scico.2013.07.002_br0330","series-title":"Predicate Calculus and Program Semantics","author":"Dijkstra","year":"1990"},{"key":"10.1016\/j.scico.2013.07.002_br0340","series-title":"Proceedings of the International Conference IFIP on Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics","first-page":"580","article-title":"Reasoning about composition using property transformers and their conjugates","author":"Charpentier","year":"2000"},{"key":"10.1016\/j.scico.2013.07.002_br0350","series-title":"Mathematics of Program Construction","first-page":"316","article-title":"Continuous action system refinement","volume":"vol. 4014","author":"Meinicke","year":"2006"},{"issue":"4","key":"10.1016\/j.scico.2013.07.002_br0360","doi-asserted-by":"crossref","first-page":"724","DOI":"10.1145\/6490.6494","article-title":"Countable nondeterminism and random assignment","volume":"33","author":"Apt","year":"1986","journal-title":"J. ACM"},{"issue":"2","key":"10.1016\/j.scico.2013.07.002_br0370","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1016\/j.scico.2006.01.007","article-title":"Modelling angelic and demonic nondeterminism with multirelations","volume":"65","author":"Martin","year":"2007","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.scico.2013.07.002_br0380","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/j.entcs.2009.12.022","article-title":"Data refinement of invariant based programs","volume":"259","author":"Preoteasa","year":"2009","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.scico.2013.07.002_br0390","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/s11225-012-9416-9","article-title":"Dual choice and iteration in an abstract algebra of action","volume":"100","author":"Solin","year":"2012","journal-title":"Stud. Log."},{"key":"10.1016\/j.scico.2013.07.002_br0400","series-title":"The Archive of Formal Proofs","first-page":"1","article-title":"Verification of the Deutsch\u2013Schorr\u2013Waite graph marking algorithm using data refinement","author":"Preoteasa","year":"2010"},{"key":"10.1016\/j.scico.2013.07.002_br0410","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/s00165-011-0195-2","article-title":"Invariant diagrams with data refinement","volume":"24","author":"Preoteasa","year":"2012","journal-title":"Form. Asp. Comput."}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/api.elsevier.com\/content\/article\/PII:S0167642313001597?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/api.elsevier.com\/content\/article\/PII:S0167642313001597?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,10,14]],"date-time":"2018-10-14T21:41:19Z","timestamp":1539553279000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642313001597"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":41,"alternative-id":["S0167642313001597"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.scico.2013.07.002","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2014,10]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Refinement algebra with dual operator","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.scico.2013.07.002","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2013 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}