{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T12:02:23Z","timestamp":1791201743783,"version":"4.2.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540388708","type":"print"},{"value":"9783540388722","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11841883_31","type":"book-chapter","created":{"date-parts":[[2006,9,19]],"date-time":"2006-09-19T11:29:11Z","timestamp":1158665351000},"page":"445-460","source":"Crossref","is-referenced-by-count":29,"title":["Weakest Preconditions for High-Level Programs"],"prefix":"10.1007","author":[{"given":"Annegret","family":"Habel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Karl-Heinz","family":"Pennemann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arend","family":"Rensink","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-28644-8_6","volume-title":"CONCUR 2004 - Concurrency Theory","author":"P. Baldan","year":"2004","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B.: Verifying finite-state graph grammars. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 83\u201398. Springer, Heidelberg (2004)"},{"key":"31_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-45832-8_4","volume-title":"Graph Transformation","author":"P. Baldan","year":"2002","unstructured":"Baldan, P., K\u00f6nig, B.: Approximating the behaviour of graph transformation systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol.\u00a02505, pp. 14\u201329. Springer, Heidelberg (2002)"},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-44898-5_14","volume-title":"Static Analysis","author":"P. Baldan","year":"2003","unstructured":"Baldan, P., K\u00f6nig, B., K\u00f6nig, B.: A logic for analyzing abstractions of graph transformation systems. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 255\u2013272. Springer, Heidelberg (2003)"},{"key":"31_CR4","unstructured":"Baldan, P., K\u00f6nig, B., Rensink, A.: Graph grammar verification through abstraction. In: K\u00f6nig, B., Montanari, U., Gardner, P. (eds.) Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. 04241 Dagstuhl Seminar Proceedings (2005)"},{"issue":"1","key":"31_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"31_CR6","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1142\/9789812384720_0003","volume-title":"Handbook of Graph Grammars and Computing by Graph Trans.","author":"A. Corradini","year":"1997","unstructured":"Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., L\u00f6we, M.: Algebraic approaches to graph transformation. In: Handbook of Graph Grammars and Computing by Graph Trans., vol.\u00a01, pp. 163\u2013245. World Scientific, Singapore (1997)"},{"key":"31_CR7","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":"31_CR8","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1989","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1989)"},{"key":"31_CR9","first-page":"125","volume":"109","author":"O.M. Santos dos","year":"2004","unstructured":"dos Santos, O.M., Dotti, F.L., Ribeiro, L.: Verifying object-based graph grammars. ENTCS\u00a0109, 125\u2013136 (2004)","journal-title":"ENTCS"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-540-39958-2_18","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"F.L. Dotti","year":"2003","unstructured":"Dotti, F.L., Foss, L., Ribeiro, L., dos Santos, O.M.: Verification of distributed object-based systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 261\u2013275. Springer, Heidelberg (2003)"},{"key":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0025714","volume-title":"Graph-Grammars and Their Application to Computer Science and Biology","author":"H. Ehrig","year":"1979","unstructured":"Ehrig, H.: Introduction to the algebraic theory of graph grammars. In: Ng, E.W., Ehrig, H., Rozenberg, G. (eds.) Graph Grammars 1978. LNCS, vol.\u00a073, pp. 1\u201369. Springer, Heidelberg (1979)"},{"key":"31_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-24721-0_16","volume-title":"Fundamental Approaches to Software Engineering","author":"H. Ehrig","year":"2004","unstructured":"Ehrig, H., Ehrig, K., De Lara, J., Taentzer, G., Varr\u00f3, D., Varr\u00f3-Gyapay, S.: Termination criteria for model transformation. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol.\u00a02984, pp. 214\u2013228. Springer, Heidelberg (2004)"},{"key":"31_CR13","unstructured":"Ehrig, H., Ehrig, K., Habel, A., Pennemann, K.-H.: Theory of constraints and application conditions: From graphs to high-level structures. Fundamenta Informaticae\u00a072 (2006)"},{"key":"31_CR14","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. EATCS Monographs of Theoretical Computer Science. Springer, Heidelberg (2006)"},{"key":"31_CR15","unstructured":"Ehrig, H., Habel, A., Padberg, J., Prange, U.: Adhesive high-level replacement systems: A new categorical framework for graph transformation. Fundamenta Informaticae\u00a072 (2006)"},{"key":"31_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-31847-7_17","volume-title":"Formal Methods in Software and Systems Modeling","author":"A. Habel","year":"2005","unstructured":"Habel, A., Pennemann, K.-H.: Nested constraints and application conditions for high-level structures. In: Kreowski, H.-J., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems Modeling. LNCS, vol.\u00a03393, pp. 293\u2013308. Springer, Heidelberg (2005)"},{"key":"31_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/11841883_30","volume-title":"Graph Transformations","author":"A. Habel","year":"2006","unstructured":"Habel, A., Pennemann, K.-H.: Satisfiability of high-level conditions. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol.\u00a04178, pp. 430\u2013444. Springer, Heidelberg (2006)"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Habel, A., Pennemann, K.-H., Rensink, A.: Weakest preconditions for high-level programs: Long version. Technical Report 8\/06, University of Oldenburg (2006)","DOI":"10.1007\/11841883_31"},{"key":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-45315-6_15","volume-title":"Foundations of Software Science and Computation Structures","author":"A. Habel","year":"2001","unstructured":"Habel, A., Plump, D.: Computational completeness of programming languages based on graph transformation. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol.\u00a02030, pp. 230\u2013245. Springer, Heidelberg (2001)"},{"key":"31_CR20","first-page":"325","volume-title":"Proc. International Conference on Principles of Knowledge Representation and Reasoning","author":"J.Y. Halpern","year":"1991","unstructured":"Halpern, J.Y., Vardi, M.Y.: Model checking vs. theorem proving: A manifesto. In: Allen, J., Fikes, R., Sandewall, E. (eds.) Proc. International Conference on Principles of Knowledge Representation and Reasoning, pp. 325\u2013334. Morgan Kaufmann, San Francisco (1991)"},{"key":"31_CR21","doi-asserted-by":"crossref","unstructured":"Heckel, R., Wagner, A.: Ensuring consistency of conditional graph grammars. In: SEGRAGRA 1995. ENTCS, vol.\u00a02, pp. 95\u2013104 (1995)","DOI":"10.1016\/S1571-0661(05)80188-4"},{"key":"31_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jcss.2004.11.002","volume":"71","author":"M. Koch","year":"2005","unstructured":"Koch, M., Mancini, L.V., Parisi-Presicce, F.: Graph-based specification of access control policies. Journal of Computer and System Sciences (JCSS)\u00a071, 1\u201333 (2005)","journal-title":"Journal of Computer and System Sciences (JCSS)"},{"key":"31_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/11691372_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. K\u00f6nig","year":"2006","unstructured":"K\u00f6nig, B., Kozioura, V.: Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 197\u2013211. Springer, Heidelberg (2006)"},{"key":"31_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/3-540-56496-9_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 164\u2013174. Springer, Heidelberg (1993)"},{"key":"31_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"issue":"2","key":"31_CR26","doi-asserted-by":"crossref","first-page":"201","DOI":"10.3233\/FI-1998-33204","volume":"33","author":"D. Plump","year":"1998","unstructured":"Plump, D.: Termination of graph rewriting is undecidable. Fundamenta Informaticae\u00a033(2), 201\u2013209 (1998)","journal-title":"Fundamenta Informaticae"},{"key":"31_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-540-30203-2_11","volume-title":"Graph Transformations","author":"D. Plump","year":"2004","unstructured":"Plump, D., Steinert, S.: Towards graph programs for graph algorithms. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol.\u00a03256, pp. 128\u2013143. Springer, Heidelberg (2004)"},{"key":"31_CR28","unstructured":"Rensink, A.: Towards model checking graph grammars. In: Leuschel, M., Gruner, S., Presti, S.L. (eds.) Workshop on Automated Verification of Critical Systems (AVoCS), Technical Report DSSE-TR-2003-2, pp. 150\u2013160. University of Southhampton (2003)"},{"key":"31_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-540-25959-6_40","volume-title":"Applications of Graph Transformations with Industrial Relevance","author":"A. Rensink","year":"2004","unstructured":"Rensink, A.: The GROOVE simulator: A tool for state space generation. In: Pfaltz, J.L., Nagl, M., B\u00f6hlen, B. (eds.) AGTIVE 2003. LNCS, vol.\u00a03062, pp. 479\u2013485. Springer, Heidelberg (2004)"},{"key":"31_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-30203-2_23","volume-title":"Graph Transformations","author":"A. Rensink","year":"2004","unstructured":"Rensink, A.: Representing first-order logic by graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol.\u00a03256, pp. 319\u2013335. Springer, Heidelberg (2004)"},{"key":"31_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-540-30203-2_17","volume-title":"Graph Transformations","author":"A. Rensink","year":"2004","unstructured":"Rensink, A., Schmidt, \u00c1., Varr\u00f3, D.: Model checking graph transformations: A comparison of two approaches. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol.\u00a03256, pp. 226\u2013241. Springer, Heidelberg (2004)"},{"key":"31_CR32","doi-asserted-by":"crossref","unstructured":"Varr\u00f3, D.: Towards symbolic analysis of visual modeling languages. ENTCS\u00a072(3) (2003)","DOI":"10.1016\/S1571-0661(04)80611-X"},{"issue":"2","key":"31_CR33","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s10270-003-0050-x","volume":"3","author":"D. Varr\u00f3","year":"2004","unstructured":"Varr\u00f3, D.: Automated formal verification of visual modeling languages by model checking. Journal of Software and Systems Modelling\u00a03(2), 85\u2013113 (2004)","journal-title":"Journal of Software and Systems Modelling"}],"container-title":["Lecture Notes in Computer Science","Graph Transformations"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11841883_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:41:00Z","timestamp":1605642060000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11841883_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540388708","9783540388722"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11841883_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}