{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:51:31Z","timestamp":1761929491980},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642120282"},{"type":"electronic","value":"9783642120299"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12029-9_16","type":"book-chapter","created":{"date-parts":[[2010,3,7]],"date-time":"2010-03-07T19:56:48Z","timestamp":1267991808000},"page":"218-232","source":"Crossref","is-referenced-by-count":3,"title":["Proving Consistency and Completeness of Model Classes Using Theory Interpretation"],"prefix":"10.1007","author":[{"given":"\u00c1d\u00e1m","family":"Darvas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Charles, J.: Adding native specifications to JML. In: FTfJP (2006)"},{"issue":"6","key":"16_CR2","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1002\/spe.649","volume":"35","author":"Y. Cheon","year":"2005","unstructured":"Cheon, Y., Leavens, G., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Software: Practice and Experience\u00a035(6), 583\u2013599 (2005)","journal-title":"Software: Practice and Experience"},{"key":"16_CR3","unstructured":"Darvas, \u00c1.: Reasoning About Data Abstraction in Contract Languages. Ph.D. thesis, ETH Zurich (2009)"},{"issue":"6","key":"16_CR4","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1049\/iet-sen:20080011","volume":"2","author":"\u00c1. Darvas","year":"2008","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Faithful mapping of model classes to mathematical structures. IET Software\u00a02(6), 477\u2013499 (2008)","journal-title":"IET Software"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/3-540-58233-9_6","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"W.M. Farmer","year":"1994","unstructured":"Farmer, W.M.: Theory interpretation in simple type theory. In: Heering, J., Meinke, K., M\u00f6ller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol.\u00a0816, pp. 96\u2013123. Springer, Heidelberg (1994)"},{"key":"16_CR6","unstructured":"Filli\u00e2tre, J.C., Hubert, T., March\u00e9, C.: The Caduceus verification tool for C programs, tutorial and Reference Manual (2007)"},{"key":"16_CR7","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"PLDI","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, vol.\u00a0\u00a037, pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"16_CR8","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"J.V. Guttag","year":"1993","unstructured":"Guttag, J.V., Horning, J.J.: Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer, Heidelberg (1993)"},{"key":"16_CR9","unstructured":"Hamilton, N., Nickson, R., Traynor, O., Utting, M.: Interpretation and instantiation of theories for reasoning about formal specifications. In: ACSC, Australian Computer Science Communications 19, pp. 37\u201345 (1997)"},{"key":"16_CR10","volume-title":"Systematic software development using VDM","author":"C.B. Jones","year":"1986","unstructured":"Jones, C.B.: Systematic software development using VDM. Prentice Hall, Englewood Cliffs (1986)"},{"issue":"1-3","key":"16_CR11","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"G.T. Leavens","year":"2005","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming\u00a055(1-3), 185\u2013205 (2005)","journal-title":"Science of Computer Programming"},{"issue":"2","key":"16_CR12","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing\u00a019(2), 159\u2013189 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"16_CR13","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"16_CR14","unstructured":"Levy, B.: An Approach to Compiler Correctness Using Interpretation Between Theories. Ph.D. thesis, University of California, Los Angeles (1986)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1007\/3-540-15199-0_14","volume-title":"Mathematical Foundations of Software Development","author":"T.S.E. Maibaum","year":"1985","unstructured":"Maibaum, T.S.E., Veloso, P.A.S., Sadler, M.R.: A theory of abstract data types for program development: bridging the gap? In: Nivat, M., Floyd, C., Thatcher, J., Ehrig, H. (eds.) CAAP 1985 and TAPSOFT 1985. LNCS, vol.\u00a0185, pp. 214\u2013230. Springer, Heidelberg (1985)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-540-73147-4_12","volume-title":"Rewriting, Computation and Proof","author":"C. March\u00e9","year":"2007","unstructured":"March\u00e9, C.: Towards modular algebraic specifications for pointer programs: a case study. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds.) Jouannaud Festschrift. LNCS, vol.\u00a04600, pp. 235\u2013258. Springer, Heidelberg (2007)"},{"key":"16_CR17","volume-title":"Eiffel: The Language","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Eiffel: The Language. Prentice Hall, Englewood Cliffs (1992)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"16_CR19","unstructured":"Object Constraint Language, OMG Available Specification, Version 2.0 (2006), http:\/\/www.omg.org\/docs\/formal\/06-05-01.pdf"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-71067-7_5","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Owre","year":"2008","unstructured":"Owre, S., Shankar, N.: A brief overview of PVS. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 22\u201327. Springer, Heidelberg (2008)"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11786160_3","volume-title":"Architecting Systems with Trustworthy Components","author":"B. Schoeller","year":"2006","unstructured":"Schoeller, B., Widmer, T., Meyer, B.: Making specifications complete through models. In: Reussner, R., Stafford, J.A., Szyperski, C. (eds.) Architecting Systems with Trustworthy Components. LNCS, vol.\u00a03938, pp. 48\u201370. Springer, Heidelberg (2006)"},{"key":"16_CR22","volume-title":"Mathematical Logic","author":"J.R. Shoenfield","year":"1967","unstructured":"Shoenfield, J.R.: Mathematical Logic. Addison-Wesley, Reading (1967)"},{"key":"16_CR23","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/3-540-60117-1_22","volume-title":"Mathematics of Program Construction","author":"Y.V. Srinivas","year":"1995","unstructured":"Srinivas, Y.V., J\u00fcllig, R.: Specware: Formal support for composing software. In: Mathematics of Program Construction, pp. 399\u2013422. Springer, Heidelberg (1995)"},{"key":"16_CR24","volume-title":"The Specification of Computer Programs","author":"W.M. Turski","year":"1987","unstructured":"Turski, W.M., Maibaum, T.S.E.: The Specification of Computer Programs. Addison-Wesley, Reading (1987)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12029-9_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T15:56:43Z","timestamp":1685462203000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12029-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120282","9783642120299"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12029-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}