{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T04:29:28Z","timestamp":1744172968735,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642332951"},{"type":"electronic","value":"9783642332968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33296-8_14","type":"book-chapter","created":{"date-parts":[[2012,9,17]],"date-time":"2012-09-17T02:24:55Z","timestamp":1347848695000},"page":"179-193","source":"Crossref","is-referenced-by-count":1,"title":["Verification Rules for Exception Handling in Eiffel"],"prefix":"10.1007","author":[{"given":"Emil","family":"Sekerinski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tian","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Eiffel: Analysis, Design and Programming Language, 2nd edn. Standard ECMA-367. Ecma International (June 2006)"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer (1998)","DOI":"10.1007\/978-1-4612-1674-2"},{"issue":"4","key":"14_CR3","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s002360050163","volume":"36","author":"R.J.R. Back","year":"1999","unstructured":"Back, R.J.R., von Wright, J.: Reasoning algebraically about loops. Acta Informatica\u00a036(4), 295\u2013334 (1999)","journal-title":"Acta Informatica"},{"issue":"5-6","key":"14_CR4","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0950-5849(95)99362-Q","volume":"37","author":"J. Bowen","year":"1995","unstructured":"Bowen, J., Gordon, M.: A shallow embedding of Z in HOL. Information and Software Technology\u00a037(5-6), 269\u2013276 (1995)","journal-title":"Information and Software Technology"},{"issue":"9","key":"14_CR5","doi-asserted-by":"publisher","first-page":"820","DOI":"10.1109\/32.877844","volume":"26","author":"P.A. Buhr","year":"2000","unstructured":"Buhr, P.A., Russell Mok, W.Y.: Advanced exception handling mechanisms. IEEE Transactions on Software Engineering\u00a026(9), 820\u2013836 (2000)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/10722010_4","volume-title":"Mathematics of Program Construction","author":"E. Cohen","year":"2000","unstructured":"Cohen, E.: Separation and Reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 45\u201359. Springer, Heidelberg (2000)"},{"issue":"2","key":"14_CR7","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1109\/TSE.1984.5010218","volume":"10","author":"F. Cristian","year":"1984","unstructured":"Cristian, F.: Correct and robust programs. IEEE Transactions on Software Engineering\u00a010(2), 163\u2013174 (1984)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-1-4612-3658-0_10","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"M.J.C. Gordon","year":"1989","unstructured":"Gordon, M.J.C.: Mechanizing programming logics in higher order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387\u2013439. Springer, New York (1989)"},{"key":"14_CR9","unstructured":"Harrison, J.: HOL Light tutorial (for version 2.20). Technical report, Intel JF1-13 (January 2011)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45309-1_19","volume-title":"Programming Languages and Systems","author":"B. Jacobs","year":"2001","unstructured":"Jacobs, B.: A Formalisation of Java\u2019s Exception Mechanism. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 284\u2013301. Springer, Heidelberg (2001)"},{"issue":"1","key":"14_CR11","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/BF01214623","volume":"7","author":"S. King","year":"1995","unstructured":"King, S., Morgan, C.: Exits in the refinement calculus. Formal Aspects of Computing\u00a07(1), 54\u201376 (1995)","journal-title":"Formal Aspects of Computing"},{"key":"14_CR12","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. SIGSOFT Software Engineering Notes\u00a031, 1\u201338 (2006)","journal-title":"SIGSOFT Software Engineering Notes"},{"key":"14_CR13","series-title":"IFIP Transactions A-56","first-page":"447","volume-title":"PROCOMET 1994: Proceedings of the IFIP TC2\/WG2.1\/WG2.2\/WG2.3 Working Conference on Programming Concepts, Methods and Calculi","author":"K.R.M. Leino","year":"1994","unstructured":"Leino, K.R.M., van de Snepscheut, J.L.A.: Semantics of exceptions. In: Olderog, E.-R. (ed.) PROCOMET 1994: Proceedings of the IFIP TC2\/WG2.1\/WG2.2\/WG2.3 Working Conference on Programming Concepts, Methods and Calculi. IFIP Transactions A-56, pp. 447\u2013466. North-Holland Publishing Co., Amsterdam (1994)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Rustan, M., Leino, K., Schulte, W.: Exception safety for C#. In: Software Engineering and Formal Methods, SEFM 2004, pp. 218\u2013227. IEEE Computer Society (2004)","DOI":"10.1109\/SEFM.2004.1347523"},{"key":"14_CR15","volume-title":"Program Development in Java: Abstraction, Specification, and Object-Oriented Design","author":"B. Liskov","year":"2000","unstructured":"Liskov, B., Guttag, J.: Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley Longman Publishing Co., Boston (2000)"},{"key":"14_CR16","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":"14_CR17","series-title":"LNBIP","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-02571-6_12","volume-title":"Objects, Components, Models and Patterns","author":"M. Nordio","year":"2009","unstructured":"Nordio, M., Calcagno, C., M\u00fcller, P., Meyer, B.: A Sound and Complete Program Logic for Eiffel. In: Oriol, M., Meyer, B. (eds.) TOOLS EUROPE 2009. LNBIP, vol.\u00a033, pp. 195\u2013214. Springer, Heidelberg (2009)"},{"key":"14_CR18","unstructured":"von Oheimb, D.: Analyzing Java in Isabelle\/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2001)"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Sekerinski, E.: Exceptions for dependability. In: Petre, L., Sere, K., Troubitsyna, E. (eds.) Dependability and Computer Engineering: Concepts for Software-Intensive Systems\u2014a Handbook on Dependability Research, pp. 11\u201335. IGI Global (2011)","DOI":"10.4018\/978-1-60960-747-0.ch002"},{"key":"14_CR20","unstructured":"Sekerinski, E., Zhang, T.: Partial correctness for exception handling. In: Bonakdarpour, B., Maibaum, T. (eds.) Proceedings of the 2nd International Workshop on Logical Aspects of Fault-Tolerance, pp. 116\u2013132 (June 2011)"},{"key":"14_CR21","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Verifying Eiffel programs with Boogie. In: Rustan, K., Leino, M., Moskal, M. (eds.) First International Workshop on Intermediate Verification Languages: BOOGIE 2011. CADE 23 Workshop, pp. 14\u201326 (2011)"},{"issue":"1-2","key":"14_CR22","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.scico.2003.09.002","volume":"51","author":"J. Wright von","year":"2004","unstructured":"von Wright, J.: Towards a refinement algebra. Science of Computer Programming\u00a051(1-2), 23\u201345 (2004); Mathematics of Program Construction (MPC 2002)","journal-title":"Science of Computer Programming"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-30142-4_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T.: Certifying Machine Code Safety: Shallow Versus Deep Embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 305\u2013320. Springer, Heidelberg (2004)"},{"issue":"2","key":"14_CR24","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1145\/3318.3320","volume":"7","author":"S. Yemini","year":"1985","unstructured":"Yemini, S., Berry, D.M.: A modular verifiable exception handling mechanism. ACM Trans. Program. Lang. Syst.\u00a07(2), 214\u2013243 (1985)","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33296-8_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T22:37:29Z","timestamp":1744151849000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33296-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642332951","9783642332968"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33296-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}