{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T16:40:16Z","timestamp":1742402416622},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540411314"},{"type":"electronic","value":"9783540400066"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40006-0_3","type":"book-chapter","created":{"date-parts":[[2007,8,11]],"date-time":"2007-08-11T09:41:54Z","timestamp":1186825314000},"page":"21-36","source":"Crossref","is-referenced-by-count":27,"title":["The Approach: Integrating Object Oriented Design and Formal Verification"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Ahrendt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Baar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernhard","family":"Beckert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Giese","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elmar","family":"Habermalz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfram","family":"Menzel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter H.","family":"Schmitt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,9,19]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B Book \u2014 Assigning Programs to Meanings. Cambridge University Press, Aug. 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"K. R. Apt. Ten years of Hoare logic: A survey \u2014 part I. ACM Transactions on Programming Languages and Systems, 1981.","DOI":"10.1145\/357146.357150"},{"key":"3_CR3","unstructured":"T. Baar. Experiences with the UML\/OCL-approach to precise software modeling: A report from practice. Submitted, see http:\/\/i12www.ira.uka.de\/~key, 2000 ."},{"key":"3_CR4","volume-title":"Softwaretechnik-Trends","author":"T. Baar","year":"2000","unstructured":"T. Baar, R. H\u00e4hnle, T. Sattler, and P. H. Schmitt. Entwurfsmustergesteuerte Erzeugung von OCL-Constraints. In G. Snelting, editor, Softwaretechnik-Trends, Informatik Aktuell. Springer, 2000."},{"key":"3_CR5","unstructured":"B. Beckert. A dynamic logic for Java Card. In Proc. 2nd ECOOP Workshop on Formal Techniques for Java Programs, Cannes, France, 2000. See http:\/\/i12www.ira.uka.de\/~key\/doc\/2000\/beckert00.pdf.gz."},{"key":"3_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/3-540-48737-9_10","volume-title":"Formal Syntax and Semantics of Java","author":"E. B\u00f6rger","year":"1999","unstructured":"E. B\u00f6rger and W. Schulte. A programmer friendly modular definition of the semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS 1523, pages 353\u2013404. Springer, 1999."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"R. Breu, R. Grosu, F. Huber, B. Rumpe, and W. Schwerin. Towards a precise semantics for object-oriented modeling techniques. In H. Kilov and B. Rumpe, editors, Proc Workshop on Precise Semantics for Object-Oriented Modeling Techniques at ECOOP\u201997. Techn. Univ. of Munich, Tech. Rep. TUM-I9725, 1997.","DOI":"10.1007\/3-540-69687-3_42"},{"issue":"4","key":"3_CR8","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E. Clarke","year":"1996","unstructured":"E. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626\u2013643, 1996.","journal-title":"ACM Computing Surveys"},{"issue":"4","key":"3_CR9","first-page":"23","volume":"29","author":"D. L. Dill","year":"1996","unstructured":"D. L. Dill and J. Rushby. Acceptance of formal methods: Lessons from hardware design. IEEE Computer, 29(4):23\u201324, 1996. Part of: Hossein Saiedian (ed.). An Invitation to Formal Methods. Pages 16\u201330.","journal-title":"IEEE Computer"},{"key":"3_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Rigorous objectoriented modeling: Integrating formal and informal notations","author":"R. B. France","year":"1997","unstructured":"R. B. France, J.-M. Bruel, M. M. Larrondo-Petrie, and E. Grant. Rigorous objectoriented modeling: Integrating formal and informal notations. In M. Johnson, editor, Proc. Algebraic Methodology and Software Technology (AMAST), Berlin, Germany, LNCS 1349. Springer, 1997."},{"key":"3_CR11","unstructured":"E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1995."},{"key":"3_CR12","unstructured":"M. Giese. Integriertes automatisches und interaktives Beweisen: Die Kalk\u00fclebene. Diploma Thesis, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, June 1998."},{"key":"3_CR13","unstructured":"M. Giese. A first-order simplification rule with constraints. In Proc. Int. Workshop on First-Order Theorem Proving, St. Andrews, Scotland, 2000. See http:\/\/i12www.ira.uka.de\/~key\/doc\/2000\/giese00a.ps.gz."},{"key":"3_CR14","unstructured":"M. Grand. Patterns in Java, volume 2. John Wiley & Sons, 1999."},{"issue":"1","key":"3_CR15","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/4236.585173","volume":"1","author":"S. B. Guthery","year":"1997","unstructured":"S. B. Guthery. Java Card: Internet computing on a smart card. IEEE Internet Computing, 1(1):57\u201359, 1997.","journal-title":"IEEE Internet Computing"},{"key":"3_CR16","unstructured":"E. Habermalz. Interactive theorem proving with schematic theory specific rules. Technical Report 19\/00, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, 2000. See http:\/\/12www.ira.uka.de\/~key\/doc\/2000\/stsr.ps.gz."},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"U. Hansmann, M. S. Nicklous, T. Sch\u00e4ck, and F. Seliger. Smart Card Application Development Using Java. Springer, 2000.","DOI":"10.1007\/978-3-642-98052-7"},{"key":"3_CR18","unstructured":"M. G. Hinchey and J. P. Bowen, editors. Applications of Formal Methods. Prentice Hall, 1995."},{"key":"3_CR19","unstructured":"I. Jacobson, G. Booch, and J. Rumbaugh. The Unified Software Development Process. Object Technology Series. Addison-Wesley, 1999."},{"key":"3_CR20","series-title":"Formal Models and Semantics","first-page":"789","volume-title":"Handbook of Theoretical Computer Science","author":"D. Kozen","year":"1990","unstructured":"D. Kozen and J. Tiuryn. Logic of programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 14, pages 789\u2013840. Elsevier, Amsterdam, 1990."},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"K. Lano. The B Language and Method: A guide to Practical Formal Development. Springer Verlag London Ltd., 1996.","DOI":"10.1007\/978-1-4471-1494-9"},{"key":"3_CR22","unstructured":"J. Martin and J. J. Odell. Object-Oriented Methods: A Foundation, UML Edition. Prentice-Hall, 1997."},{"key":"3_CR23","series-title":"Lect Notes Comput Sci","first-page":"119","volume-title":"Formal Syntax and Semantics of Java","author":"T. Nipkow","year":"1999","unstructured":"T. Nipkow and D. von Oheimb. Machine-checking the Java specification: Proving type safety. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS 1523, pages 119\u2013156. Springer, 1999."},{"key":"3_CR24","unstructured":"Object Management Group, Inc., Framingham\/MA, USA, http:\/\/www.omg.org. OMG Unified Modeling Language Specification, Version 1.3, June 1999."},{"key":"3_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer, Berlin, 1994."},{"key":"3_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"A programming logic for sequential Java","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"A. Poetzsch-Heffter and P. M\u00fcller. A programming logic for sequential Java. In S. D. Swierstra, editor, Proc. Programming Languages and Systems (ESOP), Amsterdam, The Netherlands, LNCS 1576, pages 162\u2013176. Springer, 1999."},{"key":"3_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015471","volume-title":"KORSO: Methods, Languages, and Tools for the Construction of Correct Software \u2014 Final Report","author":"W. Reif","year":"1995","unstructured":"W. Reif. The KIV-approach to software verification. In M. Broy and S. J\u00e4hnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software \u2014 Final Report, LNCS 1009. Springer, 1995."},{"key":"3_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-48257-1_25","volume-title":"Overview over the project QUEST","author":"O. Slotosch","year":"1999","unstructured":"O. Slotosch. Overview over the project QUEST. In Applied Formal Methods, Proc. FM-Trends 98, Boppard, Germany, LNCS 1641, pages 346\u2013350. Springer, 1999."},{"key":"3_CR29","unstructured":"Sun Microsystems, Inc., Palo Alto\/CA, USA. Java Card 2.1 Application Programming Interfaces, Draft 2, Release 1.3, 1998."},{"key":"3_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"586","DOI":"10.1007\/BFb0000505","volume-title":"The Cogito development system","author":"O. Traynor","year":"1997","unstructured":"O. Traynor, D. Hazel, P. Kearney, A. Martin, R. Nickson, and L. Wildman. The Cogito development system. In M. Johnson, editor, Proc. Algebraic Methodology and Software Technology, Berlin, LNCS 1349, pages 586\u2013591. Springer, 1997."},{"key":"3_CR31","unstructured":"J. Warmer and A. Kleppe. The Object Constraint Language: Precise Modelling with UML. Object Technology Series. Addison-Wesley, 1999."}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40006-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:22:46Z","timestamp":1556738566000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40006-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540411314","9783540400066"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-40006-0_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}