{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:35Z","timestamp":1775790815570,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642246890","type":"print"},{"value":"9783642246906","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24690-6_12","type":"book-chapter","created":{"date-parts":[[2011,10,24]],"date-time":"2011-10-24T21:35:37Z","timestamp":1319492137000},"page":"155-171","source":"Crossref","is-referenced-by-count":40,"title":["Reverse Hoare Logic"],"prefix":"10.1007","author":[{"given":"Edsko","family":"de Vries","sequence":"first","affiliation":[]},{"given":"Vasileios","family":"Koutavas","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K.R. Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: A survey\u2014part I. ACM Trans. Program. Lang. Syst.\u00a03, 431\u2013483 (1981)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1-2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(83)90066-X","volume":"28","author":"K.R. Apt","year":"1983","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: A survey\u2014part II: Nondeterminism. Theoretical Computer Science\u00a028(1-2), 83\u2013109 (1983)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"12_CR3","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0004-3702(94)90062-0","volume":"71","author":"F. Bacchus","year":"1994","unstructured":"Bacchus, F., Yang, Q.: Downward refinement and the efficiency of hierarchical problem solving. Artificial Intelligence\u00a071(1), 43\u2013100 (1994)","journal-title":"Artificial Intelligence"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-69149-5_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M. Barnett","year":"2008","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.S.: The spec# programming system: Challenges and directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 144\u2013152. Springer, Heidelberg (2008)"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.tcs.2007.02.040","volume":"379","author":"R. Chadha","year":"2007","unstructured":"Chadha, R., Cruz-Filipe, L., Mateus, P., Sernadas, A.: Reasoning about probabilistic sequential programs. Theor. Comput. Sci.\u00a0379, 142\u2013165 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0167-6423(90)90042-C","volume":"15","author":"W. Chen","year":"1990","unstructured":"Chen, W., Udding, J.T.: Program inversion: more than fun! Sci. Comput. Program.\u00a015, 1\u201313 (1990)","journal-title":"Comput. Program."},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D. Cok","year":"2005","unstructured":"Cok, D., Kiniry, J.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"12_CR8","unstructured":"Goldblatt, R.: Logics of time and computation. Center for the Study of Language and Information, Stanford, CA, USA (1987)"},{"key":"12_CR9","unstructured":"Harel, D.: Logics of programs: Axiomatics and descriptive power. Tech. rep., Massachusetts Institute of Technology, Cambridge, MA, USA (1978)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"den Hartog, J.: Verifying probabilistic programs using a Hoare like logic. In: Thiagarajan, P., Yap, R. (eds.) ASIAN 1999. LNCS, vol.\u00a01742, pp. 790\u2013790. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-46674-6_11"},{"key":"12_CR11","unstructured":"Heyer, T.: Semantic Inspection of Software Artifacts From Theory to Practice. Ph.D. thesis, Link\u00f6ping University (2001)"},{"key":"12_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. Commun. ACM\u00a012, 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/BF00289504","volume":"2","author":"C.A.R. Hoare","year":"1973","unstructured":"Hoare, C.A.R., Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informatica\u00a02, 335\u2013355 (1973)","journal-title":"Acta Informatica"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78663-4_1","volume-title":"Trustworthy Global Computing","author":"M. Hofmann","year":"2008","unstructured":"Hofmann, M., Pavlova, M.: Elimination of ghost variables in program logics. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol.\u00a04912, pp. 1\u201320. Springer, Heidelberg (2008)"},{"key":"12_CR15","first-page":"270","volume-title":"LICS","author":"K. Honda","year":"2005","unstructured":"Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: LICS, pp. 270\u2013279. IEEE, Los Alamitos (2005)"},{"key":"12_CR16","first-page":"39","volume-title":"ACM SIGPLAN Workshop on ML","author":"J. Kanig","year":"2009","unstructured":"Kanig, J., Filli\u00e2tre, J.C.: Who: a verifier for effectful higher-order programs. In: ACM SIGPLAN Workshop on ML, pp. 39\u201348. ACM, New York (2009)"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001650050057","volume":"11","author":"T. Kleymann","year":"1999","unstructured":"Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects of Computing\u00a011, 541\u2013566 (1999), \n                    \n                      http:\/\/dx.doi.org\/10.1007\/s001650050057\n                    \n                    \n                  , doi:10.1007\/s001650050057","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"12_CR18","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D. Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. J. Comp. and Sys. Sc.\u00a030(2), 162\u2013178 (1985)","journal-title":"J. Comp. and Sys. Sc."},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11574620_35","volume-title":"The Semantic Web \u2013 ISWC 2005","author":"A. Kumar","year":"2005","unstructured":"Kumar, A., Srivastava, B., Mittal, S.: Information modeling for end to end composition of semantic web services. In: Gil, Y., Motta, E., Benjamins, V.R., Musen, M.A. (eds.) ISWC 2005. LNCS, vol.\u00a03729, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"key":"12_CR20","volume-title":"Object-oriented software construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-oriented software construction, 2nd edn. Prentice-Hall, Inc., Upper Saddle River (1997)","edition":"2"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst., 325\u2013353 (1996)","DOI":"10.1145\/229542.229547"},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/1160074.1159812","volume":"41","author":"A. Nanevski","year":"2006","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare Type Theory. SIGPLAN Not.\u00a041, 62\u201373 (2006)","journal-title":"SIGPLAN Not."},{"key":"12_CR23","unstructured":"Ramshaw, L.H.: Formalizing the analysis of algorithms. Ph.D. thesis, Stanford University (1979)"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-45064-1_14","volume-title":"Component-Based Software Quality","author":"R. Reussner","year":"2003","unstructured":"Reussner, R., Poernomo, I., Schmidt, H.: Reasoning about software architectures with contractually specified components. In: Cechich, A., Piattini, M., Vallecillo, A. (eds.) CBSQ 2003. LNCS, vol.\u00a02693, pp. 287\u2013325. Springer, Heidelberg (2003)"},{"key":"12_CR25","first-page":"55","volume-title":"LICS","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society, Washington, DC, USA (2002)"},{"key":"12_CR26","unstructured":"ten Teije, A., van Harmelen, F.: Characterising approximate problem solving: by partially fulfilled pre- and postconditions. In: ECAI 1998. CEUR-WS, vol.\u00a016, pp. 78\u201382 (1998)"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-540-24756-2_4","volume-title":"Integrated Formal Methods","author":"J. Woodcock","year":"2004","unstructured":"Woodcock, J., Cavalcanti, A.: A Tutorial Introduction to Designs in Unifying Theories of Programming. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 40\u201366. Springer, Heidelberg (2004)"},{"issue":"2","key":"12_CR28","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0020-0190(91)90141-4","volume":"37","author":"J. Wright von","year":"1991","unstructured":"von Wright, J.: Program inversion in the refinement calculus. Information Processing Letters\u00a037(2), 95\u2013100 (1991)","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24690-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T22:12:52Z","timestamp":1555193572000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24690-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642246890","9783642246906"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24690-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}