{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:38:43Z","timestamp":1725557923050},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540250517"},{"type":"electronic","value":"9783540322542"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32254-2_27","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T19:16:54Z","timestamp":1277234214000},"page":"476-493","source":"Crossref","is-referenced-by-count":2,"title":["Verification Support Environment"],"prefix":"10.1007","author":[{"given":"Werner","family":"Stephan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Langenstein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Nonnengart","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Rock","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"27_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The Existence of Refinement Mappings. Theoretical Computer Science\u00a082(2), 253\u2013284 (1991)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"27_CR2","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems\u00a017(3), 507\u2013534 (1995)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/3-540-50214-9_8","volume-title":"VDM \u201988. VDM - The Way Ahead","author":"J.-R. Abrial","year":"1988","unstructured":"Abrial, J.-R.: The B tool. In: Goos, G., Hartmanis, J. (eds.) VDM 1988. LNCS, vol.\u00a0328, pp. 86\u201387. Springer, Heidelberg (1988)"},{"key":"27_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138, 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"27_CR5","series-title":"IFIP state-of-the-art reports","volume-title":"Algebraic foundations of systems specification","year":"1999","unstructured":"Astesiano, E., Kreowski, H.-J., Krieg-Br\u00fcckner, B. (eds.): Algebraic foundations of systems specification. IFIP state-of-the-art reports. Springer, Berlin (1999)"},{"key":"27_CR6","unstructured":"B Core UK Ltd. B-Tool manual (1994)"},{"key":"27_CR7","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W., Weise, C.: New generation of uppaal. In: International Workshop on Software Tools for Technology Transfer, Aalborg, Denmark (1998)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053349","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"D. Bert","year":"1998","unstructured":"Bert, D.: B 1998: Recent Advances in the Development and Use of the B Method. LNCS, vol.\u00a01393. Springer, Heidelberg (1998)"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"STACS 93","author":"R. Drexler","year":"1993","unstructured":"Drexler, R., Reif, W., Schellhorn, G., Stenzel, K., Stephan, W., Wolpers, A.: The KIV system: A tool for formal program development. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 1993. LNCS, vol.\u00a0665. Springer, Heidelberg (1993)"},{"key":"27_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Axiomatising the Logic of Computer Programming","author":"R. Goldblatt","year":"1982","unstructured":"Goldblatt, R.: Axiomatising the Logic of Computer Programming. LNCS, vol.\u00a0130. Springer, Heidelberg (1982)"},{"key":"27_CR11","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H.: HyTech: The cornell hybrid technology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol.\u00a0999, pp. 265\u2013293. Springer, Heidelberg (1995)"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Hutter, D., Langenstein, B., Sengler, C., Siekmann, J., Stephan, W., Wolpers, A.: Verification support environment (vse). Journal of High Integrity Systems (1995)","DOI":"10.1007\/3-540-60973-3_92"},{"key":"27_CR14","volume-title":"Proceedings Formal Methods Europe 1996: Industrial Benefits and Advances in Formal Methods","author":"D. Hutter","year":"1996","unstructured":"Hutter, D., Langenstein, B., Sengler, C., Siekmann, J.H., Stephan, W., Wolpers, A.: Deduction in the Verification Support Environment (VSE). In: Gaudel, M.-C., Woodcock, J. (eds.) Proceedings Formal Methods Europe 1996: Industrial Benefits and Advances in Formal Methods. Springer, Heidelberg (1996)"},{"issue":"6","key":"27_CR15","first-page":"523","volume":"1","author":"D. Hutter","year":"1996","unstructured":"Hutter, D., Langenstein, B., Sengler, C., Siekmann, J.H., Stephan, W., Wolpers, A.: Verification support environment (vse). High Integrity Systems\u00a01(6), 523\u2013530 (1996)","journal-title":"High Integrity Systems"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-48257-1_26","volume-title":"Applied Formal Methods - FM-Trends 98","author":"D. Hutter","year":"1999","unstructured":"Hutter, D., Mantel, H., Rock, G., Stephan, W., Wolpers, A., Balser, M., Reif, W., Schellhorn, G., Stenzel, K.: VSE: Controlling the Complexity in Formal Software Development. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol.\u00a01641, pp. 351\u2013358. Springer, Heidelberg (1999)"},{"key":"27_CR17","first-page":"367","volume-title":"FLAIRS-2000: Proceedings of the Thirteenth International Florida Artificial Intelligence Research Society Conference","author":"D. Hutter","year":"2000","unstructured":"Hutter, D., Rock, G., Siekmann, J.H., Stephan, W., Vogt, R.: Formal Software Development in the Verification Support Environment (VSE). In: Etheredge, B.M.J. (ed.) FLAIRS-2000: Proceedings of the Thirteenth International Florida Artificial Intelligence Research Society Conference, pp. 367\u2013376. AAAI-Press, Menlo Park (2000)"},{"key":"27_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - Cade-13","author":"D. Hutter","year":"1996","unstructured":"Hutter, D., Sengler, C.: INKA: The Next Generation. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104. Springer, Heidelberg (1996)"},{"key":"27_CR19","volume-title":"Systematic Software Development Using VDM","author":"C.B. Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice Hall, Englewood Cliffs (1990)","edition":"2"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems\u00a016(3) (1994)","DOI":"10.1145\/177492.177726"},{"key":"27_CR21","volume-title":"Specification of Abstract Data Types","author":"J. Loeckx","year":"1996","unstructured":"Loeckx, J., Ehrich, H.-D., Wolf, M.: Specification of Abstract Data Types. Teubner, Chichester (1996)"},{"key":"27_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)"},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"McCune, W.: Mace 2.0 reference manual and guide. Technical Memo ANL\/MCSTM- 249, Argonne National Laboratory (June 2001)","DOI":"10.2172\/797949"},{"key":"27_CR24","unstructured":"McMillan, K.: The smv model checker, http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/smv\/"},{"key":"27_CR25","series-title":"LNAI","first-page":"748","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 (LNAI), vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"27_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"ISABELLE, A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: ISABELLE, A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"27_CR27","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"27_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0023893","volume-title":"Logical Foundations of Computer Science - Tver \u201992","author":"W. Reif","year":"1992","unstructured":"Reif, W.: Correctness of generic modules. In: Nerode, A., Taitslin, M.A. (eds.) LFCS 1992. LNCS, vol.\u00a0620. Springer, Heidelberg (1992)"},{"key":"27_CR29","unstructured":"Rock, G., Stephan, W., Wolpers, A.: Tool support for the compositional development of distributed systems. In: Tagungsband 7. GI\/ITGFachgesp\u00e4ch Formale Beschreibungstechniken f\u00fcr verteilte Systeme, number 315 in GMD Studien. GMD (1997)"},{"key":"27_CR30","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/978-3-7091-6355-9_16","volume-title":"Tool Support for System Specification, Development and Verification, Advances in Computing Science","author":"G. Rock","year":"1999","unstructured":"Rock, G., Stephan, W., Wolpers, A.: Modular Reasoning about Structured TLA Specifications. In: Berghammer, R., Lakhnech, Y. (eds.) Tool Support for System Specification, Development and Verification, Advances in Computing Science, pp. 217\u2013229. Springer, WienNewYork (1999)"},{"key":"27_CR31","series-title":"International Computer Sciences Series","volume-title":"Software Engineering","author":"I. Sommerville","year":"1995","unstructured":"Sommerville, I.: Software Engineering, 5th edn. International Computer Sciences Series. Addison-Wesley, Harlow (1995)","edition":"5"},{"key":"27_CR32","series-title":"Series in Computer Science","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Series in Computer Science. Prentice Hall International, Englewood Cliffs (1992)","edition":"2"},{"key":"27_CR33","doi-asserted-by":"crossref","unstructured":"Yovine, S.: Kronos: A verification tool for real-time systems. In: Software Tools for Technology Transfer, vol.\u00a01, pp. 123\u2013133 (1997)","DOI":"10.1007\/s100090050009"}],"container-title":["Lecture Notes in Computer Science","Mechanizing Mathematical Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32254-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T09:38:09Z","timestamp":1559209089000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32254-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540250517","9783540322542"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32254-2_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}