{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:16:21Z","timestamp":1742390181677},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_8","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"100-115","source":"Crossref","is-referenced-by-count":12,"title":["Efficient Well-Definedness Checking"],"prefix":"10.1007","author":[{"given":"\u00c1d\u00e1m","family":"Darvas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Farhad","family":"Mehta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arsenii","family":"Rudich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"UML 2.0 OCL Specification (May 2006), http:\/\/www.omg.org\/docs\/formal\/06-05-01.pdf"},{"key":"8_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book: Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-45648-1_13","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J.-R. Abrial","year":"2002","unstructured":"Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 242\u2013269. Springer, Heidelberg (2002)"},{"key":"8_CR4","unstructured":"Arthan, R.: Undefinedness in Z: Issues for specification and proof. In: CADE Workshop on Mechanization of Partial Functions (1996)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2004","unstructured":"Barrett, C.W., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BF00264250","volume":"21","author":"H. Barringer","year":"1984","unstructured":"Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Informatica\u00a021, 251\u2013269 (1984)","journal-title":"Acta Informatica"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BFb0053354","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"P. Behm","year":"1998","unstructured":"Behm, P., Burdy, L., Meynadier, J.-M.: Well Defined B. In: Bert, D. (ed.) B 1998. LNCS, vol.\u00a01393, pp. 29\u201345. Springer, Heidelberg (1998)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Berezin, S., Barrett, C., Shikanian, I., Chechik, M., Gurfinkel, A., Dill, D.L.: A practical approach to partial functions in CVC Lite. In: Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2004)","DOI":"10.1016\/j.entcs.2004.06.064"},{"issue":"2","key":"8_CR10","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/s00165-006-0016-1","volume":"19","author":"P. Chalin","year":"2007","unstructured":"Chalin, P.: Are the logical foundations of verifying compiler prototypes matching user expectations? Formal Aspects of Computing\u00a019(2), 139\u2013158 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"8_CR11","first-page":"23","volume-title":"ICSE","author":"P. Chalin","year":"2007","unstructured":"Chalin, P.: A sound assertion semantics for the dependable systems evolution verifying compiler. In: ICSE, pp. 23\u201333. IEEE Computer Society Press, Los Alamitos (2007)"},{"key":"8_CR12","unstructured":"Cheng, J.H., Jones, C.B.: On the usability of logics which handle partial functions. In: Refinement Workshop, pp. 51\u201369 (1991)"},{"key":"8_CR13","unstructured":"Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A tutorial introduction to PVS. In: Workshop on Industrial-Strength Formal Specification Techniques (1995)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"TACAS","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"8_CR15","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/BFb0015254","volume-title":"Computer Science Today","author":"D. Gries","year":"1995","unstructured":"Gries, D., Schneider, F.B.: Avoiding the undefined by underspecification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 366\u2013373. Springer, Heidelberg (1995)"},{"key":"8_CR17","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)"},{"issue":"4","key":"8_CR18","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1093\/jigpal\/jzi032","volume":"13","author":"R. H\u00e4hnle","year":"2005","unstructured":"H\u00e4hnle, R.: Many-valued logic, partiality, and abstraction in formal specification languages. Logic Journal of the IGPL\u00a013(4), 415\u2013433 (2005)","journal-title":"Logic Journal of the IGPL"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1002\/malq.19790251304","volume":"25","author":"A. Hoogewijs","year":"1979","unstructured":"Hoogewijs, A.: On a formalization of the non-definedness notion. Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik\u00a025, 213\u2013217 (1979)","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"8_CR20","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)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","first-page":"108","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"J.R. Kiniry","year":"2005","unstructured":"Kiniry, J.R., Cok, D.R.: 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":"8_CR22","doi-asserted-by":"publisher","first-page":"150","DOI":"10.2307\/2267778","volume":"3","author":"S.C. Kleene","year":"1938","unstructured":"Kleene, S.C.: On a notation for ordinal numbers. Journal of Symbolic Logic\u00a03, 150\u2013155 (1938)","journal-title":"Journal of Symbolic Logic"},{"issue":"3","key":"8_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes\u00a031(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"8_CR24","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/S0049-237X(08)72018-4","volume-title":"Computer Programming and Formal Systems","author":"J. McCarthy","year":"1963","unstructured":"McCarthy, J.: A basis for a mathematical theory of computation. In: Braffort, P., Hirschberg, D. (eds.) Computer Programming and Formal Systems, pp. 33\u201370. North-Holland, Amsterdam (1963)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-540-68237-0_7","volume-title":"Formal Methods (FM)","author":"A. Rudich","year":"2008","unstructured":"Rudich, A., Darvas, \u00c1., M\u00fcller, P.: Checking well-formedness of pure-method specifications. In: Cuellar, J., Maibaum, T. (eds.) Formal Methods (FM). LNCS, vol.\u00a05014, pp. 68\u201383. Springer, Heidelberg (2008)"},{"issue":"9","key":"8_CR27","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J. Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Transactions on Software Engineering\u00a024(9), 709\u2013720 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"8_CR28","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1093\/comjnl\/42.2.73","volume":"42","author":"B. Schieder","year":"1999","unstructured":"Schieder, B., Broy, M.: Adapting calculational logic to the undefined. The Computer Journal\u00a042(2), 73\u201381 (1999)","journal-title":"The Computer Journal"},{"key":"8_CR29","volume-title":"Understanding Z: a specification language and its formal semantics","author":"J.M. Spivey","year":"1988","unstructured":"Spivey, J.M.: Understanding Z: a specification language and its formal semantics. Cambridge University Press, Cambridge (1988)"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-58156-1_18","volume-title":"Automated Deduction - CADE-12","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G., Suttner, C.B., Yemenis, T.: The TPTP Problem Library. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 252\u2013266. Springer, Heidelberg (1994)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,15]],"date-time":"2021-09-15T18:44:36Z","timestamp":1631731476000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}